diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/Makefile | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/language/Makefile b/language/Makefile index 0c7563ce..74def9cf 100644 --- a/language/Makefile +++ b/language/Makefile @@ -37,5 +37,6 @@ l2.lem: l2.ott l2_typ.ott clean: rm -rf *~ -rm -rf *.uo *.ui *.sig *.sml .HOLMK - -rm -f *.tex *.aux *.log *.dvi *.ps *.pdf + -rm -f *.aux *.log *.dvi *.ps *.pdf rm -rf l2.pdf l2_parse.pdf l2.ml l2_parse.ml l2.lem + rm -rf l2.tex doc_in.tex
\ No newline at end of file |