diff options
| author | Maxime Dénès | 2016-01-05 19:36:02 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2016-01-05 19:36:02 +0100 |
| commit | 8a9445fbf65d4ddf2c96348025d487b4d54a5d01 (patch) | |
| tree | b76decc6370803cf156429204f3c3c7944d9750c | |
| parent | e4a682e2f2c91fac47f55cd8619af2321b2e4c30 (diff) | |
Fix order of files in mllib.
CString was linked after Serialize, although the later was using CString.equal.
This had not been noticed so far because OCaml was ignoring functions marked as
external in interfaces (which is the case of CString.equal) when considering
link dependencies. This was changed on the OCaml side as part of the fix of
PR#6956, so linking was now failing in several places.
| -rw-r--r-- | Makefile.build | 5 | ||||
| -rw-r--r-- | checker/check.mllib | 4 | ||||
| -rw-r--r-- | dev/printers.mllib | 4 | ||||
| -rw-r--r-- | grammar/grammar.mllib | 4 | ||||
| -rw-r--r-- | lib/clib.mllib | 4 |
5 files changed, 11 insertions, 10 deletions
diff --git a/Makefile.build b/Makefile.build index 00ff6a7a4c..56fc5f0c7d 100644 --- a/Makefile.build +++ b/Makefile.build @@ -294,9 +294,10 @@ checker/check.cmxa: | md5chk checker/check.mllib.d # Csdp to micromega special targets ########################################################################### -plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMO:.cmo=$(BESTOBJ)) +plugins/micromega/csdpcert$(EXE): $(CSDPCERTCMO:.cmo=$(BESTOBJ)) \ + $(addsuffix $(BESTLIB), lib/clib) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,,nums unix) + $(HIDE)$(call bestocaml,,nums unix clib) ########################################################################### # CoqIde special targets diff --git a/checker/check.mllib b/checker/check.mllib index 49ca6bf051..0d36e3a0f1 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -17,6 +17,8 @@ Flags Control Pp_control Loc +CList +CString Serialize Stateid Feedback @@ -25,8 +27,6 @@ Segmenttree Unicodetable Unicode CObj -CList -CString CArray CStack Util diff --git a/dev/printers.mllib b/dev/printers.mllib index 07b48ed573..eeca6809ae 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -16,6 +16,8 @@ Backtrace IStream Pp_control Loc +CList +CString Compat Flags Control @@ -28,8 +30,6 @@ Segmenttree Unicodetable Unicode CObj -CList -CString CArray CStack Util diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 60ea0df026..71e5b8ae2c 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -16,13 +16,13 @@ Backtrace Pp_control Flags Loc +CList +CString Serialize Stateid Feedback Pp -CList -CString CArray CStack Util diff --git a/lib/clib.mllib b/lib/clib.mllib index 7ff1d29359..9c9607abdb 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -18,11 +18,11 @@ Pp_control Flags Control Loc +CList +CString Serialize Deque CObj -CList -CString CArray CStack Util |