diff -r 51eed1aefccd -r c5e32a3d7e12 doc-src/Tutorial/Makefile
--- a/doc-src/Tutorial/Makefile	Wed May 05 18:41:31 1999 +0200
+++ b/doc-src/Tutorial/Makefile	Wed May 05 18:47:37 1999 +0200
@@ -21,7 +21,6 @@
 $(NAME).dvi: $(FILES) isabelle_hol.eps
 	touch $(NAME).ind
 	$(LATEX) $(NAME)
-	$(RAIL) $(NAME)
 	$(BIBTEX) $(NAME)
 	$(LATEX) $(NAME)
 	$(LATEX) $(NAME)