aboutsummaryrefslogtreecommitdiff
path: root/configure.ml
diff options
context:
space:
mode:
authorPierre Boutillier2014-01-30 22:19:16 +0100
committerPierre Boutillier2014-02-24 14:07:06 +0100
commit5aded353dbf4eccff16769e3762c4810060fb6cf (patch)
tree44e77c4c419946c8e0596d86d6aaa92f57dcfd47 /configure.ml
parentb0b9a582d99d57d9f9c6f4b322911102cca734ff (diff)
Fix coqide build under MacOS
Diffstat (limited to 'configure.ml')
-rw-r--r--configure.ml5
1 files changed, 2 insertions, 3 deletions
diff --git a/configure.ml b/configure.ml
index 79087a4053..5488904a1e 100644
--- a/configure.ml
+++ b/configure.ml
@@ -741,7 +741,7 @@ let coqide_flags () =
let osxdir = tryrun "ocamlfind" ["query";"lablgtkosx"] in
if osxdir <> "" then begin
lablgtkincludes := sprintf "%s -I %S" !lablgtkincludes osxdir;
- idearchflags := "lablgtkosx.cmxa";
+ idearchflags := "lablgtkosx.cma";
idearchdef := "QUARTZ"
end
| "opt", "win32" ->
@@ -1113,9 +1113,8 @@ let write_makefile f =
pr "COQIDEINCLUDES=%s\n\n" !lablgtkincludes;
pr "# CoqIde (no/byte/opt)\n";
pr "HASCOQIDE=%s\n" coqide;
- pr "IDEOPTFLAGS=%s\n" !idearchflags;
+ pr "IDEFLAGS=%s\n" !idearchflags;
pr "IDEOPTDEPS=%s\n" !idearchfile;
- pr "IDEOPTINT=%s\n\n" !idearchdef;
pr "IDEINT=%s\n\n" !idearchdef;
pr "# Defining REVISION\n";
pr "CHECKEDOUT=%s\n\n" vcs;