equal
deleted
inserted
replaced
49 @$(USEDIR) -D generated -f ROOT.ML HOL Paper |
49 @$(USEDIR) -D generated -f ROOT.ML HOL Paper |
50 |
50 |
51 itp: session3 |
51 itp: session3 |
52 rm -f Paper/generated/*.aux # otherwise latex will fall over |
52 rm -f Paper/generated/*.aux # otherwise latex will fall over |
53 cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
53 cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
|
54 cd Paper/generated ; bibtex root |
|
55 cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
54 cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
56 cd Paper/generated ; $(ISABELLE_TOOL) latex -o pdf root.tex |
55 cp Paper/generated/root.pdf paper.pdf |
57 cp Paper/generated/root.pdf paper.pdf |
56 |
58 |
57 |
59 |
58 ## clean |
60 ## clean |