summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-06-01 13:41:50 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:51:43 +0200
commit61f8bbb9137a165fddaf4bcf06d0923b04ad31e7 (patch)
treed44da77808f20b1d4a0edd69a222bcebeb2aaab2
parentbbb5e6eb84a46c7e8041e05ab0059994fa0b1a25 (diff)
New upstream snapshot
-rw-r--r--debian/changelog7
-rw-r--r--debian/patches/0001-Disable-micromega-tests.patch25
-rw-r--r--debian/patches/0002-Remove-dependency-to-Unix-from-module-Profile.patch74
-rw-r--r--debian/patches/series2
4 files changed, 7 insertions, 101 deletions
diff --git a/debian/changelog b/debian/changelog
index beef4fb5..b6ddbc34 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,3 +1,10 @@
+coq (8.3~beta0+13298-1) UNRELEASED; urgency=low
+
+ * New upstream snapshot
+ - remove all patches
+
+ -- Stéphane Glondu <glondu@debian.org> Wed, 21 Jul 2010 09:51:18 +0200
+
coq (8.2.pl2+dfsg-1) unstable; urgency=low
* New upstream release
diff --git a/debian/patches/0001-Disable-micromega-tests.patch b/debian/patches/0001-Disable-micromega-tests.patch
deleted file mode 100644
index 8857a874..00000000
--- a/debian/patches/0001-Disable-micromega-tests.patch
+++ /dev/null
@@ -1,25 +0,0 @@
-From: Stephane Glondu <steph@glondu.net>
-Date: Mon, 22 Feb 2010 10:39:03 +0100
-Subject: [PATCH] Disable micromega tests
-
-Workaround for bug #570920.
----
- test-suite/check | 4 ++--
- 1 files changed, 2 insertions(+), 2 deletions(-)
-
-diff --git a/test-suite/check b/test-suite/check
-index bed86c4..e7889cf 100755
---- a/test-suite/check
-+++ b/test-suite/check
-@@ -248,8 +248,8 @@ echo "Parser tests"
- test_parser parser
- echo "Interactive tests"
- test_interactive interactive
--echo "Micromega tests"
--test_success micromega
-+#echo "Micromega tests"
-+#test_success micromega
-
- # We give a chance to disable the complexity tests which may cause
- # random build failures on build farms
---
diff --git a/debian/patches/0002-Remove-dependency-to-Unix-from-module-Profile.patch b/debian/patches/0002-Remove-dependency-to-Unix-from-module-Profile.patch
deleted file mode 100644
index 7a84720b..00000000
--- a/debian/patches/0002-Remove-dependency-to-Unix-from-module-Profile.patch
+++ /dev/null
@@ -1,74 +0,0 @@
-From: Stephane Glondu <steph@glondu.net>
-Date: Fri, 2 Jul 2010 15:00:43 +0200
-Subject: [PATCH] Remove dependency to Unix from module Profile
-
-Applied-Upstream: https://gforge.inria.fr/scm/viewvc.php?view=rev&root=coq&revision=13234
-Signed-off-by: Stephane Glondu <steph@glondu.net>
----
- Makefile.build | 4 ++--
- lib/profile.ml | 8 +++++---
- lib/profile.mli | 4 +---
- 3 files changed, 8 insertions(+), 8 deletions(-)
-
-diff --git a/Makefile.build b/Makefile.build
-index 148bb62..c4358ce 100644
---- a/Makefile.build
-+++ b/Makefile.build
-@@ -782,10 +782,10 @@ dev/printers.cma: $(PRINTERSCMO)
- parsing/grammar.cma: $(GRAMMARCMO)
- $(SHOW)'Testing $@'
- @touch test.ml4
-- $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) -I $(CAMLLIB) unix.cma $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
-+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) -I $(CAMLLIB) $(GRAMMARCMO) -impl" -impl test.ml4 -o test-grammar
- @rm -f test-grammar test.*
- $(SHOW)'OCAMLC -a $@'
-- $(HIDE)$(OCAMLC) $(BYTEFLAGS) unix.cma $(GRAMMARCMO) -linkall -a -o $@
-+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(GRAMMARCMO) -linkall -a -o $@
-
- # toplevel/mltop.ml4 (ifdef Byte)
-
-diff --git a/lib/profile.ml b/lib/profile.ml
-index dd7e977..40bfba3 100644
---- a/lib/profile.ml
-+++ b/lib/profile.ml
-@@ -17,8 +17,7 @@ let float_of_time t = float_of_int t /. 100.
- let time_of_float f = int_of_float (f *. 100.)
-
- let get_time () =
-- let {Unix.tms_utime = ut;Unix.tms_stime = st} = Unix.times () in
-- time_of_float (ut +. st)
-+ time_of_float (Sys.time ())
-
- (* Since ocaml 3.01, gc statistics are in float *)
- let get_alloc () =
-@@ -157,7 +156,10 @@ let merge_profile filename (curr_table, curr_outside, curr_total as new_data) =
- (* Unix measure of time is approximative and shoitt delays are often
- unperceivable; therefore, total times are measured in one (big)
- step to avoid rounding errors and to get the best possible
-- approximation *)
-+ approximation.
-+ Note: Sys.time is the same as:
-+ Unix.(let x = times () in x.tms_utime +. x.tms_stime)
-+ *)
-
- (*
- ---------- start profile for f1
-diff --git a/lib/profile.mli b/lib/profile.mli
-index 0937e9e..1e28834 100644
---- a/lib/profile.mli
-+++ b/lib/profile.mli
-@@ -10,12 +10,10 @@
-
- (*s This program is a small time and allocation profiler for Objective Caml *)
-
--(*i It requires the UNIX library *)
-
- (* Adapted from Christophe Raffalli *)
-
--(* To use it, link it with the program you want to profile (do not forget
--"-cclib -lunix -custom unix.cma" among the link options).
-+(* To use it, link it with the program you want to profile.
-
- To trace a function "f" you first need to get a key for it by using :
-
---
diff --git a/debian/patches/series b/debian/patches/series
deleted file mode 100644
index d368c657..00000000
--- a/debian/patches/series
+++ /dev/null
@@ -1,2 +0,0 @@
-0001-Disable-micromega-tests.patch
-0002-Remove-dependency-to-Unix-from-module-Profile.patch