doc-src/System/Makefile
changeset 10604 9bb2e34df0cd
parent 10580 930ac2bfa637
child 12464 f9d3c92eae4d
     1.1 --- a/doc-src/System/Makefile	Wed Dec 06 11:47:21 2000 +0100
     1.2 +++ b/doc-src/System/Makefile	Wed Dec 06 12:26:26 2000 +0100
     1.3 @@ -15,6 +15,8 @@
     1.4  FILES = system.tex basics.tex misc.tex fonts.tex present.tex symbols.tex \
     1.5  	../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
     1.6  
     1.7 +OUTPUT = syms.tex
     1.8 +
     1.9  syms.tex: showsymbols ../../Distribution/lib/texinputs/isabellesym.sty
    1.10  	@./showsymbols <../../Distribution/lib/texinputs/isabellesym.sty >syms.tex
    1.11