New ifdef functionality simplifies Holmakefile in computability/lambd…

…a example.
HOL-Theorem-Prover · Oct 24, 2011 · b935461 · b935461
1 parent 71b9d77
commit b935461
Showing 1 changed file with 6 additions and 10 deletions.
diff --git a/examples/computability/lambda/Holmakefile b/examples/computability/lambda/Holmakefile
@@ -1,20 +1,16 @@
 INCLUDES = ../../lambda/barendregt ../../lambda/basics \
            ../../lambda/other-models ../
 OPTIONS = QUIT_ON_FAILURE
+
+ifdef POLY
 HOLHEAP = computability-heap
 EXTRA_CLEANS = $(HOLHEAP) $(HOLHEAP).o
 
 BARE_THYS = ../../lambda/barendregt/normal_orderTheory \
             ../../lambda/other-models/pure_dBTheory
-DEPS_poly = $(patsubst %,%.uo,$(BARE_THYS))
-DEPS_mosml =
-
-TARGET_poly = $(HOLHEAP)
-TARGET_mosml = brackabs.sml
+DEPS = $(patsubst %,%.uo,$(BARE_THYS))
 
-COMM_mosml =
-COMM_poly = \
-   $(protect $(HOLDIR)/bin/buildheap) -o computability-heap $(BARE_THYS)
+$(HOLHEAP): $(DEPS)
+	$(protect $(HOLDIR)/bin/buildheap) -o computability-heap $(BARE_THYS)
 
-$(TARGET_$(ML_SYSNAME)): $(DEPS_$(ML_SYSNAME))
-	$(COMM_$(ML_SYSNAME))
+endif