diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-01-05 19:36:02 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 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 00ff6a7a4..56fc5f0c7 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 49ca6bf05..0d36e3a0f 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 07b48ed57..eeca6809a 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 60ea0df02..71e5b8ae2 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 7ff1d2935..9c9607abd 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 |