The following commit has been merged in the master branch:
commit dd1436b569216c851c4b341a127a3a7a3bf3b633
Author: Stephane Glondu [EMAIL PROTECTED]
Date: Sun Jul 27 23:19:00 2008 +0200
Switch packaging to git
diff --git a/debian/control b/debian/control
index 80f80ec..b4a9920 100644
---
The following commit has been merged in the master branch:
commit dec29bbc89ac8d0152d8464294fe9d9c131016c9
Author: Stephane Glondu [EMAIL PROTECTED]
Date: Sun Jul 27 23:20:40 2008 +0200
Add myself to Uploaders, and DM-Upload-Allowed to control
diff --git a/debian/control b/debian/control
The following commit has been merged in the master branch:
commit 8dd1802846b1f7a2304c7e63b2cf907d70f14fe1
Author: Stephane Glondu [EMAIL PROTECTED]
Date: Mon Jul 28 11:44:01 2008 +0200
Fix typo in README.Debian
diff --git a/debian/README.Debian b/debian/README.Debian
index
The following commit has been merged in the master branch:
commit db0c2d0f86e7fb2153be13431641a2fad0babf90
Author: Stephane Glondu [EMAIL PROTECTED]
Date: Mon Jul 28 11:48:45 2008 +0200
patch-stamp and configure-stamp are dependencies of build-stamp
This is needed for proper
The following commit has been merged in the master branch:
commit be8dd49cdf08dbeae0d6f36b717a54793418086b
Author: Stephane Glondu [EMAIL PROTECTED]
Date: Mon Jul 28 15:55:17 2008 +0200
Install also *.cm[iox] files
diff --git a/debian/coq.install b/debian/coq.install
index 59bcb59..c0817f7
The following commit has been merged in the master branch:
commit 3113f65a3dd4bbe1833dcf78fb21abd958dcdb04
Author: Stephane Glondu [EMAIL PROTECTED]
Date: Mon Jul 28 16:00:07 2008 +0200
ide/index_urls.txt is not there anymore
diff --git a/debian/rules b/debian/rules
index 1dc43f9..44dac55
The following commit has been merged in the master branch:
commit 10a7bc14dc87b57b022facbbbf3b31d74a4445e5
Author: Stephane Glondu [EMAIL PROTECTED]
Date: Mon Jul 28 16:02:00 2008 +0200
Add install-stamp
...so that install is not invoked twice when binary-indep and
binary-arch
The following commit has been merged in the master branch:
commit d6c7661cea5a874663179d806199634b7c4076ed
Author: Stephane Glondu [EMAIL PROTECTED]
Date: Mon Jul 28 16:02:40 2008 +0200
Fix building of (stdlib) doc
diff --git a/debian/rules b/debian/rules
index a9bd3b6..5151c91 100755
---
The following commit has been merged in the master branch:
commit cd46e5dd680be14a5f5401cfc00af3a7d2ad8847
Author: Stephane Glondu [EMAIL PROTECTED]
Date: Mon Jul 28 16:15:16 2008 +0200
Update changelog
diff --git a/debian/changelog b/debian/changelog
index 1ecb0b0..7e71877 100644
---
9 matches
Mail list logo
