summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorStephane Glondu <steph@glondu.net>2016-08-03 13:26:17 +0200
committerStephane Glondu <steph@glondu.net>2016-08-03 13:26:17 +0200
commit8b1e6080e696c8572242dfb293d755264f25cd44 (patch)
tree0448f1048ae15c91c17083cef3e341d6b7e8d73b
parent4c1533925165c08b0452559af307c742974e4b3a (diff)
Update packaging
-rw-r--r--debian/libbiniou-ocaml-dev.install.in2
1 files changed, 2 insertions, 0 deletions
diff --git a/debian/libbiniou-ocaml-dev.install.in b/debian/libbiniou-ocaml-dev.install.in
index da0de23..a4a290c 100644
--- a/debian/libbiniou-ocaml-dev.install.in
+++ b/debian/libbiniou-ocaml-dev.install.in
@@ -1,3 +1,5 @@
+@OCamlStdlibDir@/biniou/*.annot
+@OCamlStdlibDir@/biniou/*.cmt
@OCamlStdlibDir@/biniou/*.cmo
@OCamlStdlibDir@/biniou/*.cmi
@OCamlStdlibDir@/biniou/*.ml*