From e2d34ac167e510b718aeb696b006718d36e8ae71 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 10 Aug 2015 15:54:24 +0200
Subject: [PATCH] Cope with installation of *.cmt and *.cmti files

---
 debian/gen_modules.pl | 5 +++++
 1 file changed, 5 insertions(+)

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";
         }
-- 
2.30.2