From 54d1aa1493c9e058fc765a3c812da85ca3330693 Mon Sep 17 00:00:00 2001
From: Peter Sewell
Date: Mon, 30 Jan 2017 10:29:35 +0000
Subject: remove "rm *.tex" from language/Makefile "make clean"

---
 language/Makefile | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3