The following commit has been merged in the master branch:
commit e14f48f3c4c4a15a58da69df085908b2350db61a
Author: Stephane Glondu st...@glondu.net
Date: Sat Mar 3 12:00:25 2012 +0100
Remove useless references to quilt
diff --git a/debian/control b/debian/control
index 3e97319..62fcde5
The following commit has been merged in the master branch:
commit f7ffae599975a383420c70ee6f3fcfba935c99fc
Author: Stephane Glondu st...@glondu.net
Date: Sat Mar 3 12:28:58 2012 +0100
Switch patches to git-based patches
diff --git a/debian/patches/0001-Add-DESTDIR.patch
The following commit has been merged in the master branch:
commit 0d666992ccba0788498636d7d63ac2a8d0b0e582
Author: Stephane Glondu st...@glondu.net
Date: Sat Mar 3 12:32:12 2012 +0100
Add compatibility with camlp5 strict
diff --git
3 matches
Mail list logo
