doc-src/System/Makefile

--- a/doc-src/System/Makefile	Wed Dec 06 11:47:21 2000 +0100
+++ b/doc-src/System/Makefile	Wed Dec 06 12:26:26 2000 +0100
@@ -15,6 +15,8 @@
 FILES = system.tex basics.tex misc.tex fonts.tex present.tex symbols.tex \
 	../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
 
+OUTPUT = syms.tex
+
 syms.tex: showsymbols ../../Distribution/lib/texinputs/isabellesym.sty
 	@./showsymbols <../../Distribution/lib/texinputs/isabellesym.sty >syms.tex