doc-src/System/Makefile
changeset 28224 10487d954a8f
parent 28221 ca9fdab0f971
child 28226 97c530dc8aca
equal deleted inserted replaced
28223:eee194395fdc 28224:10487d954a8f
    10 ## dependencies
    10 ## dependencies
    11 
    11 
    12 include ../Makefile.in
    12 include ../Makefile.in
    13 
    13 
    14 NAME = system
    14 NAME = system
    15 FILES = system.tex Thy/document/Basics.tex misc.tex		\
    15 FILES = system.tex Thy/document/Basics.tex Thy/document/Misc.tex \
    16 	Thy/document/Presentation.tex symbols.tex ../iman.sty	\
    16 	Thy/document/Presentation.tex symbols.tex ../iman.sty	 \
    17 	../extra.sty ../ttbox.sty ../manual.bib
    17 	../extra.sty ../ttbox.sty ../manual.bib			 \
    18 
    18 
    19 OUTPUT = syms.tex
    19 OUTPUT = syms.tex
    20 
    20 
    21 syms.tex: showsymbols ../isabellesym.sty
    21 syms.tex: showsymbols ../isabellesym.sty
    22 	@./showsymbols <../isabellesym.sty >syms.tex
    22 	@./showsymbols <../isabellesym.sty >syms.tex