projects / helm.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 3b4ce4f)
fixed missing -syntax when using ocamlopt
authorEnrico Tassi <enrico.tassi@inria.fr>
Tue, 24 May 2005 14:14:28 +0000 (14:14 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Tue, 24 May 2005 14:14:28 +0000 (14:14 +0000)
helm/ocaml/cic_notation/Makefile patch | blob | history

diff --git a/helm/ocaml/cic_notation/Makefile b/helm/ocaml/cic_notation/Makefile
index 8a168568f804172e4fc28923ab3291eea6f8a0fa..fcf53edd5535eda996394cfbec8f23e7b49c4db3 100644 (file)
--- a/helm/ocaml/cic_notation/Makefile
+++ b/helm/ocaml/cic_notation/Makefile
@@ -27,8 +27,8 @@ test_parser: test_parser.ml $(PACKAGE).cma
 
 cicNotationLexer.cmo: OCAMLC = $(OCAMLC_P4)
 cicNotationParser.cmo: OCAMLC = $(OCAMLC_P4)
-cicNotationLexer.cmx: OCAMLC = $(OCAMLC_P4)
-cicNotationParser.cmx: OCAMLC = $(OCAMLC_P4)
+cicNotationLexer.cmx: OCAMLOPT = $(OCAMLOPT_P4)
+cicNotationParser.cmx: OCAMLOPT = $(OCAMLOPT_P4)
 
 clean: extra_clean
 distclean: extra_clean
Unnamed repository; edit this file 'description' to name the repository.