aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--coq-mathcomp-algebra.opam3
-rw-r--r--coq-mathcomp-character.opam3
-rw-r--r--coq-mathcomp-field.opam3
-rw-r--r--coq-mathcomp-fingroup.opam3
-rw-r--r--coq-mathcomp-solvable.opam3
-rw-r--r--coq-mathcomp-ssreflect.opam1
-rwxr-xr-xetc/utils/packager3
7 files changed, 6 insertions, 13 deletions
diff --git a/coq-mathcomp-algebra.opam b/coq-mathcomp-algebra.opam
index c6c5568..bea2a70 100644
--- a/coq-mathcomp-algebra.opam
+++ b/coq-mathcomp-algebra.opam
@@ -1,5 +1,4 @@
opam-version: "2.0"
-name: "coq-mathcomp-algebra"
version: "dev"
maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
@@ -10,7 +9,7 @@ license: "CeCILL-B"
build: [ make "-C" "mathcomp/algebra" "-j" "%{jobs}%" ]
install: [ make "-C" "mathcomp/algebra" "install" ]
-depends: [ "coq-mathcomp-fingroup" { = "dev" } ]
+depends: [ "coq-mathcomp-fingroup" { = version } ]
tags: [ "keyword:algebra" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.algebra" ]
authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ]
diff --git a/coq-mathcomp-character.opam b/coq-mathcomp-character.opam
index 4e64b60..f87418a 100644
--- a/coq-mathcomp-character.opam
+++ b/coq-mathcomp-character.opam
@@ -1,5 +1,4 @@
opam-version: "2.0"
-name: "coq-mathcomp-character"
version: "dev"
maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
@@ -10,7 +9,7 @@ license: "CeCILL-B"
build: [ make "-C" "mathcomp/character" "-j" "%{jobs}%" ]
install: [ make "-C" "mathcomp/character" "install" ]
-depends: [ "coq-mathcomp-field" { = "dev" } ]
+depends: [ "coq-mathcomp-field" { = version } ]
tags: [ "keyword:algebra" "keyword:character" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.character" ]
authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ]
diff --git a/coq-mathcomp-field.opam b/coq-mathcomp-field.opam
index bdde3ce..a893ca1 100644
--- a/coq-mathcomp-field.opam
+++ b/coq-mathcomp-field.opam
@@ -1,5 +1,4 @@
opam-version: "2.0"
-name: "coq-mathcomp-field"
version: "dev"
maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
@@ -10,7 +9,7 @@ license: "CeCILL-B"
build: [ make "-C" "mathcomp/field" "-j" "%{jobs}%" ]
install: [ make "-C" "mathcomp/field" "install" ]
-depends: [ "coq-mathcomp-solvable" { = "dev" } ]
+depends: [ "coq-mathcomp-solvable" { = version } ]
tags: [ "keyword:algebra" "keyword:field" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.field" ]
authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ]
diff --git a/coq-mathcomp-fingroup.opam b/coq-mathcomp-fingroup.opam
index 3e39c4e..e2993db 100644
--- a/coq-mathcomp-fingroup.opam
+++ b/coq-mathcomp-fingroup.opam
@@ -1,5 +1,4 @@
opam-version: "2.0"
-name: "coq-mathcomp-fingroup"
version: "dev"
maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
@@ -10,7 +9,7 @@ license: "CeCILL-B"
build: [ make "-C" "mathcomp/fingroup" "-j" "%{jobs}%" ]
install: [ make "-C" "mathcomp/fingroup" "install" ]
-depends: [ "coq-mathcomp-ssreflect" { = "dev" } ]
+depends: [ "coq-mathcomp-ssreflect" { = version } ]
tags: [ "keyword:finite groups" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.fingroup" ]
authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ]
diff --git a/coq-mathcomp-solvable.opam b/coq-mathcomp-solvable.opam
index ac561a5..242b05e 100644
--- a/coq-mathcomp-solvable.opam
+++ b/coq-mathcomp-solvable.opam
@@ -1,5 +1,4 @@
opam-version: "2.0"
-name: "coq-mathcomp-solvable"
version: "dev"
maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
@@ -10,7 +9,7 @@ license: "CeCILL-B"
build: [ make "-C" "mathcomp/solvable" "-j" "%{jobs}%" ]
install: [ make "-C" "mathcomp/solvable" "install" ]
-depends: [ "coq-mathcomp-algebra" { = "dev" } ]
+depends: [ "coq-mathcomp-algebra" { = version } ]
tags: [ "keyword:finite groups" "keyword:Feit Thompson theorem" "keyword:small scale reflection" "keyword:mathematical components" "keyword:odd order theorem" "logpath:mathcomp.solvable" ]
authors: [ "Jeremy Avigad <>" "Andrea Asperti <>" "Stephane Le Roux <>" "Yves Bertot <>" "Laurence Rideau <>" "Enrico Tassi <>" "Ioana Pasca <>" "Georges Gonthier <>" "Sidi Ould Biha <>" "Cyril Cohen <>" "Francois Garillot <>" "Alexey Solovyev <>" "Russell O'Connor <>" "Laurent Théry <>" "Assia Mahboubi <>" ]
diff --git a/coq-mathcomp-ssreflect.opam b/coq-mathcomp-ssreflect.opam
index 28b9e31..35f0997 100644
--- a/coq-mathcomp-ssreflect.opam
+++ b/coq-mathcomp-ssreflect.opam
@@ -1,5 +1,4 @@
opam-version: "2.0"
-name: "coq-mathcomp-ssreflect"
version: "dev"
maintainer: "Mathematical Components <mathcomp-dev@sympa.inria.fr>"
diff --git a/etc/utils/packager b/etc/utils/packager
index 408172c..9a83647 100755
--- a/etc/utils/packager
+++ b/etc/utils/packager
@@ -72,8 +72,7 @@ do pkgdir="$PKGPREFIX/coq-mathcomp-$pkg/coq-mathcomp-$pkg.$VERSION"
if [ $VERSION == "dev" ]
then cp $GITROOT/coq-mathcomp-$pkg.opam $pkgdir/opam
else git show "$BRANCH:coq-mathcomp-$pkg.opam" > $pkgdir/opam
- sed -r "/^version/s?dev?$VERSION?" -i $pkgdir/opam
- sed -r "/^depends.*coq-mathcomp.*/s?dev?$VERSION?" -i $pkgdir/opam
+ sed -r "/^version/d" -i $pkgdir/opam
fi
echo "" >> $pkgdir/opam
echo "url {" >> $pkgdir/opam