doc-src/System/Makefile
changeset 28224 10487d954a8f
parent 28221 ca9fdab0f971
child 28226 97c530dc8aca
     1.1 --- a/doc-src/System/Makefile	Mon Sep 15 19:43:10 2008 +0200
     1.2 +++ b/doc-src/System/Makefile	Mon Sep 15 20:22:38 2008 +0200
     1.3 @@ -12,9 +12,9 @@
     1.4  include ../Makefile.in
     1.5  
     1.6  NAME = system
     1.7 -FILES = system.tex Thy/document/Basics.tex misc.tex		\
     1.8 -	Thy/document/Presentation.tex symbols.tex ../iman.sty	\
     1.9 -	../extra.sty ../ttbox.sty ../manual.bib
    1.10 +FILES = system.tex Thy/document/Basics.tex Thy/document/Misc.tex \
    1.11 +	Thy/document/Presentation.tex symbols.tex ../iman.sty	 \
    1.12 +	../extra.sty ../ttbox.sty ../manual.bib			 \
    1.13  
    1.14  OUTPUT = syms.tex
    1.15