symlink automagically cicReduction.ml if it doesn't exist

diff --git a/helm/ocaml/cic_proof_checking/Makefile b/helm/ocaml/cic_proof_checking/Makefile
index 95ce4ad15a4268b92830271a9c5c4d724d9d13d3..eb8bd271318886609a4225f74200164ea80f8642 100644 (file)
--- a/helm/ocaml/cic_proof_checking/Makefile
+++ b/helm/ocaml/cic_proof_checking/Makefile
@@ -2,6 +2,8 @@ PACKAGE = cic_proof_checking
 REQUIRES = helm-cic
 PREDICATES =
 
+REDUCTION_IMPLEMENTATION = cicReductionNaif.ml
+
 INTERFACE_FILES = logger.mli cicEnvironment.mli cicPp.mli cicSubstitution.mli \
                   cicMiniReduction.mli cicReductionNaif.mli cicReduction.mli \
                   cicTypeChecker.mli
@@ -13,5 +15,13 @@ EXTRA_OBJECTS_TO_INSTALL = \
             cicMiniReduction.cmo cicMiniReduction.cmx cicMiniReduction.o
 EXTRA_OBJECTS_TO_CLEAN =
 
-
 include ../Makefile.common
+
+cicReduction.ml: $(REDUCTION_IMPLEMENTATION)
+       if ! [ -f $@ ]; then \
+               echo "Using $< for $@"; \
+               ln -s $< $@;    \
+       else    \
+               true;   \
+       fi
+