From: Stephane Glondu <steph@glondu.net>
Date: Mon, 10 Aug 2015 13:54:24 +0000 (+0200)
Subject: Cope with installation of *.cmt and *.cmti files
X-Git-Tag: archive/raspbian/4.08.1-4+rpi1~3^2~138
X-Git-Url: https://dgit.raspbian.org/?a=commitdiff_plain;h=e2d34ac167e510b718aeb696b006718d36e8ae71;p=ocaml.git

Cope with installation of *.cmt and *.cmti files
---

diff --git a/debian/gen_modules.pl b/debian/gen_modules.pl
index aa03393f..9706ae32 100755
--- a/debian/gen_modules.pl
+++ b/debian/gen_modules.pl
@@ -55,6 +55,7 @@ while (<>) {
                 print_if_existing("${prefix}.o");
                 print_if_existing("${prefix}.p.cmx");
                 print_if_existing("${prefix}.p.o");
+                print_if_existing("${prefix}.p.cmt");
             }
         } elsif ($ext eq "cmxa") {
             if ($opt_arch) {
@@ -63,6 +64,10 @@ while (<>) {
                 print_if_existing("${prefix}.p.cmxa");
                 print_if_existing("${prefix}.p.a");
             }
+        } elsif ($ext eq "ml") {
+          print "${prefix}.ml\n";
+          print_if_existing("${prefix}.cmt");
+          print_if_existing("${prefix}.cmti");
         } else {
             print "${prefix}.${ext}\n";
         }