equal
deleted
inserted
replaced
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 fonts.tex present.tex symbols.tex \ |
16 ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib |
16 ../iman.sty ../extra.sty ../ttbox.sty ../manual.bib |
|
17 |
|
18 OUTPUT = syms.tex |
17 |
19 |
18 syms.tex: showsymbols ../../Distribution/lib/texinputs/isabellesym.sty |
20 syms.tex: showsymbols ../../Distribution/lib/texinputs/isabellesym.sty |
19 @./showsymbols <../../Distribution/lib/texinputs/isabellesym.sty >syms.tex |
21 @./showsymbols <../../Distribution/lib/texinputs/isabellesym.sty >syms.tex |
20 |
22 |
21 dvi: $(NAME).dvi |
23 dvi: $(NAME).dvi |