diff options
| author | Peter Sewell | 2017-01-30 10:29:35 +0000 |
|---|---|---|
| committer | Peter Sewell | 2017-01-30 10:29:35 +0000 |
| commit | 54d1aa1493c9e058fc765a3c812da85ca3330693 (patch) | |
| tree | 3cda2a8e4e9ff749f1e27ecc3365960442190efa | |
| parent | 0189ef186771a7f5ea40a750dc0b9922ff8adbf5 (diff) | |
remove "rm *.tex" from language/Makefile "make clean"
| -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 |