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

diff --git a/debian/gen_modules.pl b/debian/gen_modules.pl
index aa03393f6f5a92a30027e919affa7ec73ed73c66..9706ae32d226b0c78894b8f723e024fa9aed3556 100755 (executable)
--- 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";
         }