huge commit regarding the grafite_status:

[helm.git] / helm / software / matita / Makefile

diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile
index e822326d489c2fc4002dc8a7f52bb60f67b6bf24..d8d81bf3713159caa7007221f6cd0922f7a13d9f 100644 (file)
--- a/helm/software/matita/Makefile
+++ b/helm/software/matita/Makefile
@@ -11,7 +11,7 @@ else
   ANNOTOPTION =
 endif
 
-OCAML_FLAGS = -pp $(CAMLP5O) -rectypes $(ANNOTOPTION)
+OCAML_FLAGS = -pp $(CAMLP5O) -rectypes $(ANNOTOPTION) 
 OCAMLDEP_FLAGS = -pp $(CAMLP5O) 
 PKGS = -package "$(MATITA_REQUIRES)"
 CPKGS = -package "$(MATITA_CREQUIRES)"