--- a/doc-src/HOL/Makefile Mon May 10 17:43:55 1999 +0200 +++ b/doc-src/HOL/Makefile Mon May 10 17:44:17 1999 +0200 @@ -5,7 +5,6 @@ ## targets default: dvi -dist: dvi ## dependencies