Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more accurate cleanup;
authorwenzelm
Thu, 05 Nov 2009 16:23:51 +0100
changeset 33450 4389ec600ba7
parent 33449 9a4b176292ec
child 33451 64205e046dca
more accurate cleanup;
src/HOL/IsaMakefile file | annotate | diff | comparison | revisions
src/HOLCF/IsaMakefile file | annotate | diff | comparison | revisions
src/ZF/IsaMakefile file | annotate | diff | comparison | revisions 
--- a/src/HOL/IsaMakefile	Thu Nov 05 15:55:07 2009 +0100
+++ b/src/HOL/IsaMakefile	Thu Nov 05 16:23:51 2009 +0100
@@ -1420,28 +1420,38 @@
 ## clean
 
 clean:
-	@rm -f $(OUT)/HOL-Plain $(OUT)/HOL-Main $(OUT)/HOL		\
-		$(OUT)/HOL-Nominal $(OUT)/TLA $(LOG)/HOL.gz		\
-		$(LOG)/TLA.gz $(LOG)/HOL-Isar_Examples.gz		\
-		$(LOG)/HOL-Induct.gz $(LOG)/HOL-ex.gz			\
-		$(LOG)/HOL-Subst.gz $(LOG)/HOL-IMP.gz			\
-		$(LOG)/HOL-IMPP.gz $(LOG)/HOL-Hoare.gz			\
-		$(LOG)/HOL-Hoare_Parallel.gz $(LOG)/HOL-Lex.gz		\
-		$(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz		\
-		$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Modelcheck.gz		\
-		$(LOG)/HOL-Lambda.gz $(LOG)/HOL-Bali.gz			\
-		$(LOG)/HOL-MicroJava.gz $(LOG)/HOL-NanoJava.gz		\
-		$(OUT)/HOL-Multivariate_Analysis			\
-		$(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-IOA.gz	\
-		$(LOG)/HOL-Lattice $(LOG)/HOL-Matrix			\
-		$(LOG)/HOL-Hahn_Banach.gz $(LOG)/HOL-SET_Protocol.gz	\
-		$(LOG)/TLA-Inc.gz $(LOG)/TLA-Buffer.gz			\
-		$(LOG)/TLA-Memory.gz $(LOG)/HOL-Library.gz		\
-		$(LOG)/HOL-Unix.gz $(OUT)/HOL-Word $(LOG)/HOL-Word.gz	\
-		$(LOG)/HOL-Word-Examples.gz $(OUT)/HOL-NSA		\
-		$(LOG)/HOL-NSA.gz $(LOG)/HOL-NSA-Examples.gz		\
-		$(LOG)/HOL-Mirabelle.gz $(OUT)/HOL-SMT			\
-		$(LOG)/HOL-SMT.gz $(LOG)/HOL-SMT-Examples.gz 		\
-		$(OUT)/HOL-Boogie $(LOG)/HOL-Boogie.gz 			\
-		$(LOG)/HOL-Boogie-Examples.gz
-
+	@rm -f $(LOG)/HOL-Algebra.gz $(LOG)/HOL-Auth.gz			\
+		$(LOG)/HOL-Bali.gz $(LOG)/HOL-Base.gz			\
+		$(LOG)/HOL-Boogie-Examples.gz $(LOG)/HOL-Boogie.gz	\
+		$(LOG)/HOL-Decision_Procs.gz $(LOG)/HOL-Extraction.gz	\
+		$(LOG)/HOL-Hahn_Banach.gz $(LOG)/HOL-Hoare.gz		\
+		$(LOG)/HOL-Hoare_Parallel.gz $(LOG)/HOL-IMP.gz		\
+		$(LOG)/HOL-IMPP.gz $(LOG)/HOL-IOA.gz			\
+		$(LOG)/HOL-Imperative_HOL.gz $(LOG)/HOL-Import.gz	\
+		$(LOG)/HOL-Induct.gz $(LOG)/HOL-Isar_Examples.gz	\
+		$(LOG)/HOL-Lambda.gz $(LOG)/HOL-Lattice			\
+		$(LOG)/HOL-Lattice.gz $(LOG)/HOL-Lex.gz			\
+		$(LOG)/HOL-Library.gz $(LOG)/HOL-Main.gz		\
+		$(LOG)/HOL-Matrix $(LOG)/HOL-Matrix.gz			\
+		$(LOG)/HOL-Metis_Examples.gz $(LOG)/HOL-MicroJava.gz	\
+		$(LOG)/HOL-Mirabelle.gz $(LOG)/HOL-Modelcheck.gz	\
+		$(LOG)/HOL-Multivariate_Analysis.gz			\
+		$(LOG)/HOL-NSA-Examples.gz $(LOG)/HOL-NSA.gz		\
+		$(LOG)/HOL-NanoJava.gz $(LOG)/HOL-Nitpick_Examples.gz	\
+		$(LOG)/HOL-Nominal-Examples.gz $(LOG)/HOL-Nominal.gz	\
+		$(LOG)/HOL-Number_Theory.gz				\
+		$(LOG)/HOL-Old_Number_Theory.gz $(LOG)/HOL-Plain.gz	\
+		$(LOG)/HOL-Probability.gz $(LOG)/HOL-Prolog.gz		\
+		$(LOG)/HOL-SET_Protocol.gz $(LOG)/HOL-SMT-Examples.gz	\
+		$(LOG)/HOL-SMT.gz $(LOG)/HOL-SizeChange.gz		\
+		$(LOG)/HOL-Statespace.gz $(LOG)/HOL-Subst.gz		\
+		$(LOG)/HOL-UNITY.gz $(LOG)/HOL-Unix.gz			\
+		$(LOG)/HOL-W0.gz $(LOG)/HOL-Word-Examples.gz		\
+		$(LOG)/HOL-Word.gz $(LOG)/HOL-ZF.gz $(LOG)/HOL-ex.gz	\
+		$(LOG)/HOL.gz $(LOG)/HOL4.gz $(LOG)/TLA-Buffer.gz	\
+		$(LOG)/TLA-Inc.gz $(LOG)/TLA-Memory.gz $(LOG)/TLA.gz	\
+		$(OUT)/HOL $(OUT)/HOL-Algebra $(OUT)/HOL-Base		\
+		$(OUT)/HOL-Boogie $(OUT)/HOL-Main			\
+		$(OUT)/HOL-Multivariate_Analysis $(OUT)/HOL-NSA		\
+		$(OUT)/HOL-Nominal $(OUT)/HOL-Plain $(OUT)/HOL-SMT	\
+		$(OUT)/HOL-Word $(OUT)/HOL4 $(OUT)/TLA
--- a/src/HOLCF/IsaMakefile	Thu Nov 05 15:55:07 2009 +0100
+++ b/src/HOLCF/IsaMakefile	Thu Nov 05 16:23:51 2009 +0100
@@ -187,7 +187,8 @@
 ## clean
 
 clean:
-	@rm -f $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz \
-	  $(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz \
-          $(OUT)/IOA $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz \
-	  $(LOG)/IOA-NTP.gz $(LOG)/IOA-Modelcheck.gz $(LOG)/IOA-Storage.gz
+	@rm -f $(OUT)/HOLCF $(LOG)/HOLCF.gz $(LOG)/HOLCF-IMP.gz	\
+	  $(LOG)/HOLCF-ex.gz $(LOG)/HOLCF-FOCUS.gz $(OUT)/IOA	\
+	  $(LOG)/IOA.gz $(LOG)/IOA-ABP.gz $(LOG)/IOA-NTP.gz	\
+	  $(LOG)/IOA-Modelcheck.gz $(LOG)/IOA-Storage.gz	\
+	  $(LOG)/IOA-ex.gz
--- a/src/ZF/IsaMakefile	Thu Nov 05 15:55:07 2009 +0100
+++ b/src/ZF/IsaMakefile	Thu Nov 05 16:23:51 2009 +0100
@@ -143,7 +143,7 @@
 ## clean
 
 clean:
-	@rm -f $(OUT)/ZF $(LOG)/ZF.gz $(LOG)/ZF-AC.gz $(LOG)/ZF-Coind.gz \
-	  $(LOG)/ZF-Constructible.gz $(LOG)/ZF-ex.gz \
-          $(LOG)/ZF-IMP.gz $(LOG)/ZF-Resid.gz \
-	  $(LOG)/ZF-UNITY.gz
+	@rm -f $(OUT)/ZF $(LOG)/ZF.gz $(LOG)/ZF-AC.gz		\
+	  $(LOG)/ZF-Coind.gz $(LOG)/ZF-Constructible.gz		\
+	  $(LOG)/ZF-ex.gz $(LOG)/ZF-IMP.gz $(LOG)/ZF-Induct.gz	\
+	  $(LOG)/ZF-Resid.gz $(LOG)/ZF-UNITY.gz
isabelle