diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-05-27 19:47:33 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2017-05-27 19:47:33 +0200 |
| commit | 7d5873c1008a458247517d0c6200c0004340fd63 (patch) | |
| tree | 13f1cbe8ed70a4438d24e1993d97876e7f89df7b /test-suite/coq-makefile/coqdoc1 | |
| parent | 9c8cdd5f6c1cb4bda2f8558c17df3ffe69c49264 (diff) | |
coq_makefile: build .cma for each .mlpack
It used to generate only .cmo (the packed one).
While this works if the plugin has no external dependencies,
it does not if it does.
The bug affected only bytecode builds
Diffstat (limited to 'test-suite/coq-makefile/coqdoc1')
| -rwxr-xr-x | test-suite/coq-makefile/coqdoc1/run.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/coq-makefile/coqdoc1/run.sh b/test-suite/coq-makefile/coqdoc1/run.sh index e071f1db7..7d82f5fae 100755 --- a/test-suite/coq-makefile/coqdoc1/run.sh +++ b/test-suite/coq-makefile/coqdoc1/run.sh @@ -15,6 +15,7 @@ make install-doc DSTROOT="$PWD/tmp" sort -u > desired <<EOT . ./test +./test/test_plugin.cma ./test/test_plugin.cmi ./test/test_plugin.cmo ./test/test_plugin.cmx |