diff --git a/doc/Makefile b/doc/Makefile index bde890d..d117076 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -6,10 +6,10 @@ PIC2PLOT=/app/plotutils/bin/pic2plot NETPBM=/app/netpbm/bin GS=/app/gs DESTDIR=/dds/pubs/web/home/sw/umlgraph -THREAD=/dds/pubs/courses/intro/thread.pl +NOTETOOLS=/dds/pubs/courses/tools GIF := $(shell sed -n 's/.*$@