aboutsummaryrefslogtreecommitdiff
path: root/test-suite/coq-makefile/findlib-package/findlib
diff options
context:
space:
mode:
authorMaxime Dénès2017-08-31 09:09:00 +0200
committerMaxime Dénès2017-08-31 09:09:00 +0200
commit596f4f0ef2883f712bfe5d664a59912becb61a8d (patch)
tree1dd6d7821b9d1f8922d45ea4b0ab5efb496b55f5 /test-suite/coq-makefile/findlib-package/findlib
parentbdaf7032912feabf5ee97af33bf32e4359ad2d25 (diff)
parent5cba636c873a93367cd3f26fd0efc919e68ddc5a (diff)
Merge PR #958: coq_makefile: build/use .cma for packed plugins too
Diffstat (limited to 'test-suite/coq-makefile/findlib-package/findlib')
-rw-r--r--test-suite/coq-makefile/findlib-package/findlib/foo/META4
-rw-r--r--test-suite/coq-makefile/findlib-package/findlib/foo/Makefile14
-rw-r--r--test-suite/coq-makefile/findlib-package/findlib/foo/foo.mli0
-rw-r--r--test-suite/coq-makefile/findlib-package/findlib/foo/foolib.ml2
4 files changed, 20 insertions, 0 deletions
diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/META b/test-suite/coq-makefile/findlib-package/findlib/foo/META
new file mode 100644
index 0000000000..ff5f1c7c96
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package/findlib/foo/META
@@ -0,0 +1,4 @@
+archive(byte)="foo.cma"
+archive(native)="foo.cmxa"
+linkopts="-linkall"
+requires="str"
diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile b/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile
new file mode 100644
index 0000000000..31cf116652
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package/findlib/foo/Makefile
@@ -0,0 +1,14 @@
+-include ../../Makefile.conf
+
+CO=$(COQMF_OCAMLFIND) opt
+CB=$(COQMF_OCAMLFIND) ocamlc
+
+all:
+ $(CO) -c foolib.ml
+ $(CO) -a foolib.cmx -o foo.cmxa
+ $(CB) -c foolib.ml
+ $(CB) -a foolib.cmo -o foo.cma
+ $(CB) -c foo.mli # empty .mli file, to be understood
+
+clean:
+ rm -f *.cmo *.cma *.cmx *.cmxa *.cmi *.o *.a
diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/foo.mli b/test-suite/coq-makefile/findlib-package/findlib/foo/foo.mli
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package/findlib/foo/foo.mli
diff --git a/test-suite/coq-makefile/findlib-package/findlib/foo/foolib.ml b/test-suite/coq-makefile/findlib-package/findlib/foo/foolib.ml
new file mode 100644
index 0000000000..81306fb89b
--- /dev/null
+++ b/test-suite/coq-makefile/findlib-package/findlib/foo/foolib.ml
@@ -0,0 +1,2 @@
+let foo () =
+ assert(Str.search_forward (Str.regexp "foo") "barfoobar" 0 = 3)