doc-src/System/Makefile
changeset 12464 f9d3c92eae4d
parent 10604 9bb2e34df0cd
child 27631 b9ec32fb5f63
equal deleted inserted replaced
12463:52e4de17734e 12464:f9d3c92eae4d
    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 basics.tex misc.tex fonts.tex present.tex symbols.tex \
    15 FILES = system.tex basics.tex misc.tex present.tex symbols.tex \
    16 	../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
    16 	../iman.sty ../extra.sty ../ttbox.sty ../manual.bib
    17 
    17 
    18 OUTPUT = syms.tex
    18 OUTPUT = syms.tex
    19 
    19 
    20 syms.tex: showsymbols ../../Distribution/lib/texinputs/isabellesym.sty
    20 syms.tex: showsymbols ../../Distribution/lib/texinputs/isabellesym.sty