summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-12-01 11:26:53 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2010-12-01 13:36:59 +0100
commitca297726cd05e93f49e69ec798140b2ee77304b3 (patch)
tree84145dfc90f7bf619a15e17bf6fca3fb9da6f3e3
parentaa51449cb692a9a1d183b2663679645aba16b036 (diff)
New upstream release
-rw-r--r--debian/changelog7
-rw-r--r--debian/patches/0001-Fix-Makefile-generation.patch94
-rw-r--r--debian/patches/series1
3 files changed, 7 insertions, 95 deletions
diff --git a/debian/changelog b/debian/changelog
index 6359894..06d08a9 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,10 @@
+aac-tactics (0.2.1-1) UNRELEASED; urgency=low
+
+ * New upstream release
+ - remove patch (applied upstream)
+
+ -- Stéphane Glondu <glondu@debian.org> Wed, 01 Dec 2010 13:36:22 +0100
+
aac-tactics (0.1-r13244-1) experimental; urgency=low
* Initial release (Closes: #605487)
diff --git a/debian/patches/0001-Fix-Makefile-generation.patch b/debian/patches/0001-Fix-Makefile-generation.patch
deleted file mode 100644
index bf654fe..0000000
--- a/debian/patches/0001-Fix-Makefile-generation.patch
+++ /dev/null
@@ -1,94 +0,0 @@
-From: Stephane Glondu <steph@glondu.net>
-Date: Mon, 29 Nov 2010 23:52:39 +0100
-Subject: [PATCH] Fix Makefile generation
-
- * add "#!" header to make_makefile
- * add "-R . AACTactics" option to coq_makefile, and adapt theory.ml
- * add custom rule for aac_tactics.cmxa
- * fix Makefile rule
- * fix build on bytecode/non-natdynlink architectures
- * workaround Coq bug #2444
-
-Signed-off-by: Stephane Glondu <steph@glondu.net>
----
- magic.txt | 1 +
- make_makefile | 22 ++++++++++++++++++----
- theory.ml | 2 +-
- 3 files changed, 20 insertions(+), 5 deletions(-)
-
-diff --git a/magic.txt b/magic.txt
-index d0272c3..1b17df7 100644
---- a/magic.txt
-+++ b/magic.txt
-@@ -1,4 +1,5 @@
- -custom "mkdir -p doc; $(CAMLBIN)ocamldoc -html -rectypes -d doc -m A $(ZDEBUG) $(ZFLAGS) $^ && touch doc" "$(MLIFILES)" doc
- -custom "$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -linkall -o aac_tactics.cmxs $(CMXFILES)" "$(CMXFILES)" aac_tactics.cmxs
- -custom "$(CAMLLINK) -g -a -o aac_tactics.cma $(CMOFILES)" "$(CMOFILES)" aac_tactics.cma
-+-custom "$(CAMLOPTLINK) -g -a -o aac_tactics.cmxa $(CMXFILES)" "$(CMXFILES)" aac_tactics.cmxa
- -custom "$(CAMLBIN)ocamldep -slash $(OCAMLLIBS) $^ > .depend" "$(MLIFILES)" .depend
-diff --git a/make_makefile b/make_makefile
-index 3cfc096..44b47f1 100755
---- a/make_makefile
-+++ b/make_makefile
-@@ -1,3 +1,4 @@
-+#!/bin/sh
- # - set variable MLIFILES so that it can be used in custom targets to
- # build documentation and dependencies for .mli files
- # - remove useless ' -I . .../plugins/ ' lines so that we can read something in the compilation log
-@@ -5,9 +6,22 @@
- # - patch the rule for cleaning doc
- # - include the .depend custom target, to take .mli dependencies into account
-
-+set -e
-+
-+if [ -f `ocamlc -where`/dynlink.cmxa ]; then
-+ BEST=opt
-+ CMXA=aac_tactics.cmxa
-+ CMXS=aac_tactics.cmxs
-+else
-+ BEST=byte
-+ if which ocamlopt >/dev/null; then
-+ CMXA=aac_tactics.cmxa
-+ fi
-+fi
-+
- (
--coq_makefile -no-install -opt MLIFILES = '$(MLFILES:.ml=.mli)' $(cat files.txt) -f magic.txt \
-- | sed 's|.*/plugins/.*||g;s|Makefile:|\.dummy:|g;s|rm -f doc|rm -rf doc|g'
-+coq_makefile -R . AACTactics -no-install -$BEST MLIFILES = '$(MLFILES:.ml=.mli)' $(cat files.txt) -f magic.txt \
-+ | sed 's|.*/plugins/.*||g;s|Makefile:|\.dummy:|g;s|rm -f doc|rm -rf doc|g;s|\.opt||g'
- cat <<EOF
-
- # sanity checks
-@@ -15,7 +29,7 @@ tests: Tests.vo
-
- # override inadequate coq_makefile auto-regeneration
- Makefile: make_makefile magic.txt files.txt
-- . make_makefile
-+ ./make_makefile
-
- # We want to keep the proofs only in the Tutorial
- tutorial: Tutorial.vo Tutorial.glob
-@@ -28,7 +42,7 @@ world: \$(VOFILES) doc gallinahtml tutorial
- # ignores this dependency)
- # (one can safely select one of theses dependencies according to
- # coq' compilation mode--bytecode or native)
--AAC.vo: aac_tactics.cmxs aac_tactics.cma
-+AAC.vo: $CMXA $CMXS aac_tactics.cma
-
-
- # .depend contains dependencies for .mli files
-diff --git a/theory.ml b/theory.ml
-index 45a76f1..f2041da 100644
---- a/theory.ml
-+++ b/theory.ml
-@@ -16,7 +16,7 @@
-
- open Term
-
--let ac_theory_path = ["AAC"]
-+let ac_theory_path = ["AACTactics"; "AAC"]
-
- module Sigma = struct
- let sigma = lazy (Coq.init_constant ac_theory_path "sigma")
---
diff --git a/debian/patches/series b/debian/patches/series
deleted file mode 100644
index 649ecb9..0000000
--- a/debian/patches/series
+++ /dev/null
@@ -1 +0,0 @@
-0001-Fix-Makefile-generation.patch