summaryrefslogtreecommitdiff
path: root/debian/patches
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-09-07 18:58:27 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-09-08 00:16:26 +0200
commitb6db9f4f71b806d89cd24db386a6bcdd3b469d31 (patch)
tree98434e63efec4e958e54e22a63130b391f497033 /debian/patches
parentcdce320e124a3fcba458fad3c638940ce8f993ce (diff)
Remove obsolete patches
Diffstat (limited to 'debian/patches')
-rw-r--r--debian/patches/00list4
-rwxr-xr-xdebian/patches/check.dpatch19
-rwxr-xr-xdebian/patches/no-complexity-test.dpatch21
-rwxr-xr-xdebian/patches/non-native-archs.dpatch32
-rwxr-xr-xdebian/patches/use-env-in-coq-config.dpatch24
5 files changed, 0 insertions, 100 deletions
diff --git a/debian/patches/00list b/debian/patches/00list
index fb3801fa..e69de29b 100644
--- a/debian/patches/00list
+++ b/debian/patches/00list
@@ -1,4 +0,0 @@
-no-complexity-test
-check
-use-env-in-coq-config
-non-native-archs
diff --git a/debian/patches/check.dpatch b/debian/patches/check.dpatch
deleted file mode 100755
index d0cb3907..00000000
--- a/debian/patches/check.dpatch
+++ /dev/null
@@ -1,19 +0,0 @@
-#! /bin/sh /usr/share/dpatch/dpatch-run
-## check.dpatch by Samuel Mimram <smimram@debian.org>
-##
-## All lines beginning with `## DP:' are a description of the patch.
-## DP: Suppress warnings from tests outputs.
-
-@DPATCH@
-diff -urNad coq~/test-suite/check coq/test-suite/check
---- coq~/test-suite/check 2008-07-25 15:36:31.000000000 +0200
-+++ coq/test-suite/check 2008-07-25 15:36:31.000000000 +0200
-@@ -52,7 +52,7 @@
- nbtests=`expr $nbtests + 1`
- printf " "$f"..."
- tmpoutput=`mktemp /tmp/coqcheck.XXXXXX`
-- $command $f 2>&1 | grep -v "Welcome to Coq" | grep -v "Skipping rcfile loading" > $tmpoutput
-+ $command $f 2>&1 | grep -v "Welcome to Coq" | grep -v "Skipping rcfile loading" | grep -v "some rule has been masked" > $tmpoutput
- foutput=`dirname $f`/`basename $f .v`.out
- diff $tmpoutput $foutput >& /dev/null
- if [ $? = 0 ]; then
diff --git a/debian/patches/no-complexity-test.dpatch b/debian/patches/no-complexity-test.dpatch
deleted file mode 100755
index 5f9bff67..00000000
--- a/debian/patches/no-complexity-test.dpatch
+++ /dev/null
@@ -1,21 +0,0 @@
-#! /bin/sh /usr/share/dpatch/dpatch-run
-## no-complexity-test.dpatch by Julien Cristau <julien.cristau@ens-lyon.org>
-##
-## All lines beginning with `## DP:' are a description of the patch.
-## DP: Don't run complexity tests, they are far too fragile.
-
-@DPATCH@
-diff -urNad coq~/test-suite/check coq/test-suite/check
---- coq~/test-suite/check 2008-07-25 15:13:00.000000000 +0200
-+++ coq/test-suite/check 2008-07-25 15:33:55.000000000 +0200
-@@ -250,8 +250,8 @@
- test_interactive interactive
- echo "Micromega tests"
- test_success micromega
--echo "Complexity tests"
--test_complexity complexity
-+echo "Skipping complexity tests"
-+#test_complexity complexity
- echo "Module tests"
- $coqtop -compile modules/Nat
- $coqtop -compile modules/plik
diff --git a/debian/patches/non-native-archs.dpatch b/debian/patches/non-native-archs.dpatch
deleted file mode 100755
index cbb9f832..00000000
--- a/debian/patches/non-native-archs.dpatch
+++ /dev/null
@@ -1,32 +0,0 @@
-#! /bin/sh /usr/share/dpatch/dpatch-run
-## non-native-archs.dpatch by Stephane Glondu <steph@glondu.net>
-##
-## All lines beginning with `## DP:' are a description of the patch.
-## DP: Fix FTBFS on non-native architectures
-
-@DPATCH@
-diff --git a/Makefile.build b/Makefile.build
-index a5bae4e..c47b688 100644
---- a/Makefile.build
-+++ b/Makefile.build
-@@ -655,7 +655,10 @@ install-library:
- $(MKDIR) $(FULLCOQLIB)/states
- $(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states
- $(MKDIR) $(FULLCOQLIB)/user-contrib
-- $(INSTALLLIB) $(LINKCMO) $(LINKCMX) $(GRAMMARCMA) $(FULLCOQLIB)
-+ $(INSTALLLIB) $(LINKCMO) $(GRAMMARCMA) $(FULLCOQLIB)
-+ifeq ($(BEST),opt)
-+ $(INSTALLLIB) $(LINKCMX) $(FULLCOQLIB)
-+endif
- find . -name \*.cmi -exec $(INSTALLLIB) {} $(FULLCOQLIB) \;
-
- install-library-light:
-@@ -716,7 +719,7 @@ dev/printers.cma: $(PRINTERSCMO)
- parsing/grammar.cma: $(GRAMMARCMO)
- $(SHOW)'Testing $@'
- @touch test.ml4
-- $(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
-+ $(HIDE)$(OCAMLC) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
- @rm -f test-grammar test.*
- $(SHOW)'OCAMLC -a $@'
- $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@
diff --git a/debian/patches/use-env-in-coq-config.dpatch b/debian/patches/use-env-in-coq-config.dpatch
deleted file mode 100755
index 1f01315f..00000000
--- a/debian/patches/use-env-in-coq-config.dpatch
+++ /dev/null
@@ -1,24 +0,0 @@
-#! /bin/sh /usr/share/dpatch/dpatch-run
-## use-env-in-coq-config.dpatch by Stephane Glondu <steph@glondu.net>
-##
-## All lines beginning with `## DP:' are a description of the patch.
-## DP: Use environment variables by default in coq_config.ml
-
-@DPATCH@
-diff --git a/configure b/configure
-index 2747ee2..a57b996 100755
---- a/configure
-+++ b/configure
-@@ -862,9 +862,9 @@ cat << END_OF_COQ_CONFIG > $mlconfig_file
- (* DO NOT EDIT THIS FILE: automatically generated by ../configure *)
-
- let local = $local
--let bindir = "$ESCBINDIR"
--let coqlib = "$ESCLIBDIR"
--let coqtop = "$ESCCOQTOP"
-+let bindir = try Sys.getenv "COQBIN" with Not_found -> "$ESCBINDIR"
-+let coqlib = try Sys.getenv "COQLIB" with Not_found -> "$ESCLIBDIR"
-+let coqtop = try Sys.getenv "COQTOP" with Not_found -> "$ESCCOQTOP"
- let camldir = "$ESCCAMLDIR"
- let camllib = "$ESCCAMLLIB"
- let camlp4 = "$CAMLP4"