# HG changeset patch
# User krauss
# Date 1301239945 -7200
# Node ID e54a985daa6152623682018c77a57aa7a29fd4e9
# Parent  6803f2fd15c1f5d3383d6c26b1b3176e73ab4d9b
added make target 'smlnj' to refer to what can/should be tested using smlnj -- allows the use of "isabelle makeall smlnj";
adapted test configuration SML_makeall

diff -r 6803f2fd15c1 -r e54a985daa61 Admin/mira.py
--- a/Admin/mira.py	Sun Mar 27 16:56:16 2011 +0200
+++ b/Admin/mira.py	Sun Mar 27 17:32:25 2011 +0200
@@ -347,4 +347,4 @@
 @configuration(repos = [Isabelle], deps = [])
 def SML_makeall(*args):
     """Makeall built with SML/NJ"""
-    return isabelle_makeall(*args, more_settings=smlnj_settings, make_options=('-j', '3'))
+    return isabelle_makeall(*args, more_settings=smlnj_settings, target='smlnj', make_options=('-j', '3'))
diff -r 6803f2fd15c1 -r e54a985daa61 src/CCL/IsaMakefile
--- a/src/CCL/IsaMakefile	Sun Mar 27 16:56:16 2011 +0200
+++ b/src/CCL/IsaMakefile	Sun Mar 27 17:32:25 2011 +0200
@@ -8,6 +8,7 @@
 images: CCL
 test: CCL-ex
 all: images test
+smlnj: all
 
 
 ## global settings
diff -r 6803f2fd15c1 -r e54a985daa61 src/CTT/IsaMakefile
--- a/src/CTT/IsaMakefile	Sun Mar 27 16:56:16 2011 +0200
+++ b/src/CTT/IsaMakefile	Sun Mar 27 17:32:25 2011 +0200
@@ -8,6 +8,7 @@
 images: CTT
 test: CTT-ex
 all: images test
+smlnj: all
 
 
 ## global settings
diff -r 6803f2fd15c1 -r e54a985daa61 src/Cube/IsaMakefile
--- a/src/Cube/IsaMakefile	Sun Mar 27 16:56:16 2011 +0200
+++ b/src/Cube/IsaMakefile	Sun Mar 27 17:32:25 2011 +0200
@@ -8,6 +8,7 @@
 images:
 test: Pure-Cube
 all: images test
+smlnj: all
 
 
 ## global settings
diff -r 6803f2fd15c1 -r e54a985daa61 src/FOL/IsaMakefile
--- a/src/FOL/IsaMakefile	Sun Mar 27 16:56:16 2011 +0200
+++ b/src/FOL/IsaMakefile	Sun Mar 27 17:32:25 2011 +0200
@@ -8,6 +8,7 @@
 images: FOL
 test: FOL-ex
 all: images test
+smlnj: all
 
 
 ## global settings
diff -r 6803f2fd15c1 -r e54a985daa61 src/FOLP/IsaMakefile
--- a/src/FOLP/IsaMakefile	Sun Mar 27 16:56:16 2011 +0200
+++ b/src/FOLP/IsaMakefile	Sun Mar 27 17:32:25 2011 +0200
@@ -8,6 +8,7 @@
 images: FOLP
 test: FOLP-ex
 all: images test
+smlnj: all
 
 
 ## global settings
diff -r 6803f2fd15c1 -r e54a985daa61 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sun Mar 27 16:56:16 2011 +0200
+++ b/src/HOL/IsaMakefile	Sun Mar 27 17:32:25 2011 +0200
@@ -15,7 +15,6 @@
   HOL-Multivariate_Analysis \
   HOL-NSA \
   HOL-Nominal \
-  HOL-Probability \
   HOL-Proofs \
   HOL-SPARK \
   HOL-Word \
@@ -27,13 +26,11 @@
   HOL-Main \
   HOL-Plain
 
-#Note: keep targets sorted (except for HOL-ex)
+#Note: keep targets sorted
 test: \
-  HOL-ex \
   HOL-Auth \
   HOL-Bali \
   HOL-Boogie-Examples \
-  HOL-Decision_Procs \
   HOL-Hahn_Banach \
   HOL-Hoare \
   HOL-Hoare_Parallel \
@@ -62,14 +59,12 @@
   HOL-Mutabelle \
   HOL-NanoJava \
   HOL-Nitpick_Examples \
-  HOL-Nominal-Examples \
   HOL-Number_Theory \
   HOL-Old_Number_Theory \
   HOL-Quotient_Examples \
   HOL-Predicate_Compile_Examples \
   HOL-Prolog \
   HOL-Proofs-ex \
-  HOL-Proofs-Extraction \
   HOL-Proofs-Lambda \
   HOL-SET_Protocol \
   HOL-SPARK-Examples \
@@ -85,8 +80,17 @@
   HOL-ZF
     # ^ this is the sort position
 
-all: test images
+images-no-smlnj: \
+  HOL-Probability
 
+test-no-smlnj: \
+  HOL-ex \
+  HOL-Decision_Procs \
+  HOL-Proofs-Extraction \
+  HOL-Nominal-Examples
+
+all: test-no-smlnj test images-no-smlnj images
+smlnj: test images
 
 ## global settings
 
diff -r 6803f2fd15c1 -r e54a985daa61 src/LCF/IsaMakefile
--- a/src/LCF/IsaMakefile	Sun Mar 27 16:56:16 2011 +0200
+++ b/src/LCF/IsaMakefile	Sun Mar 27 17:32:25 2011 +0200
@@ -8,6 +8,7 @@
 images: LCF
 test: LCF-ex
 all: images test
+smlnj: all
 
 
 ## global settings
diff -r 6803f2fd15c1 -r e54a985daa61 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Sun Mar 27 16:56:16 2011 +0200
+++ b/src/Pure/IsaMakefile	Sun Mar 27 17:32:25 2011 +0200
@@ -8,6 +8,7 @@
 images: Pure
 test: RAW
 all: images test
+smlnj: all
 
 
 ## global settings
diff -r 6803f2fd15c1 -r e54a985daa61 src/Sequents/IsaMakefile
--- a/src/Sequents/IsaMakefile	Sun Mar 27 16:56:16 2011 +0200
+++ b/src/Sequents/IsaMakefile	Sun Mar 27 17:32:25 2011 +0200
@@ -8,6 +8,7 @@
 images: Sequents
 test: Sequents-LK
 all: images test
+smlnj: all
 
 
 ## global settings
diff -r 6803f2fd15c1 -r e54a985daa61 src/ZF/IsaMakefile
--- a/src/ZF/IsaMakefile	Sun Mar 27 16:56:16 2011 +0200
+++ b/src/ZF/IsaMakefile	Sun Mar 27 17:32:25 2011 +0200
@@ -10,6 +10,7 @@
 #Note: keep targets sorted
 test: ZF-AC ZF-Coind ZF-Constructible ZF-IMP ZF-Induct ZF-Resid ZF-UNITY ZF-ex
 all: images test
+smlnj: all
 
 
 ## global settings