diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/addentry.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/tools/addentry.ml b/tools/addentry.ml index 79dd687..21f5d6f 100644 --- a/tools/addentry.ml +++ b/tools/addentry.ml @@ -15,11 +15,8 @@ let file_index : int = 1 let format = format_of_string " -PDFTEX ?= pdflatex -HTMLTEX ?= htlatex - .PHONY: %s -%s: +%s: clean $(HTMLTEX) source/%s/paper.tex $(PDFTEX) source/%s/paper.tex " |