The following commit has been merged in the master branch:
commit 331f53499e751f658e32e2beb98336f454c5c0c2
Author: Stephane Glondu <[EMAIL PROTECTED]>
Date: Fri Aug 8 23:20:12 2008 +0200
Update debian/changelog
diff --git a/debian/changelog b/debian/changelog
index 10148c5..48d98bb 100644
-
The following commit has been merged in the master branch:
commit ff20e3e9f517cba61a94103d62e284b214fe4d30
Author: Stephane Glondu <[EMAIL PROTECTED]>
Date: Fri Aug 8 23:14:15 2008 +0200
Tune clean target of debian/rules
diff --git a/debian/rules b/debian/rules
index 50a6e64..7a986d9 100755
The following commit has been merged in the master branch:
commit e6b699f7e1a1ba63c1eb7b7e63094cad633791a9
Author: Stephane Glondu <[EMAIL PROTECTED]>
Date: Fri Aug 8 17:57:55 2008 +0200
Install csdpcert
diff --git a/debian/coq.install b/debian/coq.install
index c0817f7..0648440 100644
---
The following commit has been merged in the master branch:
commit a88339e768ad1c3c36250dff659120236b900cf0
Author: Stephane Glondu <[EMAIL PROTECTED]>
Date: Fri Aug 8 16:48:51 2008 +0200
glob.dump is not there anymore
diff --git a/debian/rules b/debian/rules
index e50ad14..50a6e64 100755
--
The following commit has been merged in the master branch:
commit 280b58b25462cd9f8e33f96ff76e84cf22eb465c
Author: Stephane Glondu <[EMAIL PROTECTED]>
Date: Fri Aug 8 15:29:35 2008 +0200
Move patch-stamp as a prerequisite of configure-stamp
diff --git a/debian/rules b/debian/rules
index 807
The following commit has been merged in the master branch:
commit ad9b0fc2f2c0945eb48ae6d9cd7256b11dfd8792
Author: Stephane Glondu <[EMAIL PROTECTED]>
Date: Fri Aug 8 16:47:33 2008 +0200
Remove Encoding from debian/coqide.desktop
...as complained by Lintian
diff --git a/debian/coqi
The following commit has been merged in the master branch:
commit 9fd4621dcafc03b56c348a0342b2d172c065121d
Author: Stephane Glondu <[EMAIL PROTECTED]>
Date: Fri Aug 8 15:25:39 2008 +0200
Add use-env-in-coq-config.dpatch
Use environment variables by default in coq_config.ml. This all
The following commit has been merged in the master branch:
commit dbb8a5704033fb6990af449e29c6018286d4b044
Author: Stephane Glondu <[EMAIL PROTECTED]>
Date: Fri Aug 8 13:28:00 2008 +0200
Disable compiling/installing doc
diff --git a/debian/rules b/debian/rules
index cd34b8b..8075e71 100755
The following commit has been merged in the master branch:
commit 38db629f4be6f0a963b95a958a99bbe382b6b5d1
Author: Stephane Glondu <[EMAIL PROTECTED]>
Date: Fri Aug 8 15:41:29 2008 +0200
Remove browser.dpatch and use --browser configure option
diff --git a/debian/patches/00list b/debian/pat
The following commit has been merged in the master branch:
commit 1950fa2f34bb93fe514e9035284073221c1cbba6
Author: Stephane Glondu <[EMAIL PROTECTED]>
Date: Fri Aug 8 13:20:02 2008 +0200
New upstream release
diff --git a/debian/changelog b/debian/changelog
index 677e23d..10148c5 100644
---
The following commit has been merged in the master branch:
commit bd4bb27ee4f66b08434d9a199f00b04ccec34722
Merge: db4ea6ddcbeb0dea41267dc87a30b76a01e402af
870075f34dd9fa5792bfbf413afd3b96f17e76a0
Author: Stephane Glondu <[EMAIL PROTECTED]>
Date: Fri Aug 8 13:18:48 2008 +0200
Merge commit 'u
11 matches
Mail list logo
