The following commit has been merged in the master branch:
commit 46514403cc300ea5b0666406dce11caf2cb03024
Author: Mehdi Dogguy <me...@debian.org>
Date: Mon Jan 2 15:58:09 2012 +0100
Fix mess created by 37a8809
diff --git a/debian/patches/0001-Why-2.29-do-support-Coq-8.3.patch
b/debian/patches/0001-Why-2.29-do-support-Coq-8.3.patch
index 675b564..62068cf 100644
--- a/debian/patches/0001-Why-2.29-do-support-Coq-8.3.patch
+++ b/debian/patches/0001-Why-2.29-do-support-Coq-8.3.patch
@@ -7,7 +7,7 @@ Subject: Why 2.29 do support Coq 8.3
1 files changed, 1 insertions(+), 1 deletions(-)
diff --git a/tools/dpConfig.ml b/tools/dpConfig.ml
-index e298bcf..a2068e5 100644
+index e298bcf..66be764 100644
--- a/tools/dpConfig.ml
+++ b/tools/dpConfig.ml
@@ -221,7 +221,7 @@ let coq =
diff --git a/debian/patches/0002-Mark-alt-ergo-0.93-as-compatible.patch
b/debian/patches/0002-Mark-alt-ergo-0.93-as-compatible.patch
index a2b00b0..1738e0e 100644
--- a/debian/patches/0002-Mark-alt-ergo-0.93-as-compatible.patch
+++ b/debian/patches/0002-Mark-alt-ergo-0.93-as-compatible.patch
@@ -7,7 +7,7 @@ Subject: Mark alt-ergo > 0.93 as compatible
1 files changed, 1 insertions(+), 1 deletions(-)
diff --git a/tools/dpConfig.ml b/tools/dpConfig.ml
-index a2068e5..8266412 100644
+index 66be764..da10db6 100644
--- a/tools/dpConfig.ml
+++ b/tools/dpConfig.ml
@@ -84,7 +84,7 @@ let alt_ergo =
diff --git a/debian/patches/0005-Fix-Jc_annot_inference-use-old_reg_pos.patch
b/debian/patches/0005-Fix-Jc_annot_inference-use-old_reg_pos.patch
index cdb459b..5d8c520 100644
--- a/debian/patches/0005-Fix-Jc_annot_inference-use-old_reg_pos.patch
+++ b/debian/patches/0005-Fix-Jc_annot_inference-use-old_reg_pos.patch
@@ -7,7 +7,7 @@ Subject: Fix Jc_annot_inference (use old_reg_pos)
1 files changed, 1 insertions(+), 1 deletions(-)
diff --git a/jc/jc_annot_inference.ml b/jc/jc_annot_inference.ml
-index d9dbbd7..08e66e4 100644
+index d9dbbd7..0d3143e 100644
--- a/jc/jc_annot_inference.ml
+++ b/jc/jc_annot_inference.ml
@@ -491,7 +491,7 @@ let reg_annot ?id ?kind ?name ~pos ~anchor a =
diff --git a/debian/patches/0006-Fix-spelling-error-in-binary.patch
b/debian/patches/0006-Fix-spelling-error-in-binary.patch
new file mode 100644
index 0000000..31cbda9
--- /dev/null
+++ b/debian/patches/0006-Fix-spelling-error-in-binary.patch
@@ -0,0 +1,36 @@
+From: Mehdi Dogguy <me...@debian.org>
+Date: Mon, 2 Jan 2012 15:57:10 +0100
+Subject: Fix spelling-error-in-binary
+
+---
+ src/smtlib.ml | 2 +-
+ tools/dp.ml | 2 +-
+ 2 files changed, 2 insertions(+), 2 deletions(-)
+
+diff --git a/src/smtlib.ml b/src/smtlib.ml
+index 7c99f9d..3dcfe16 100644
+--- a/src/smtlib.ml
++++ b/src/smtlib.ml
+@@ -311,7 +311,7 @@ let print_obligation fmt loc _is_lemma _o s =
+ fprintf fmt "@]@\n@\n"
+ (*
+
+- useless since goals are splitted
++ useless since goals are split
+ (moreover, may trigger a bug with Z3: proves the lemma using the
aussmption given after)
+
+ if is_lemma then begin
+diff --git a/tools/dp.ml b/tools/dp.ml
+index c09f436..b672d8e 100644
+--- a/tools/dp.ml
++++ b/tools/dp.ml
+@@ -72,7 +72,7 @@ let spec =
+ "-select", Arg.Set select_hypotheses,
+ "applies some selection of hypotheses (only Alt-Ergo)";
+ "-simple", Arg.Set simple, "Print only Valid, I don't know, Invalid,
Fail, Timeout";
+- "-split", Arg.Set split, "Create a directory wich contains all the goal
splitted in different file";
++ "-split", Arg.Set split, "Create a directory wich contains all the goal
split in different file";
+ "-prover", Arg.Symbol (
+ ["Alt-Ergo";"CVC3";"CVCL";"Z3";"Yices";"Simplify";"Vampire";
"VeriT"],(fun s -> prover := Some s)), "Select the prover to use"
+ ]
+--
diff --git a/debian/patches/series b/debian/patches/series
index 3642552..189bddd 100644
--- a/debian/patches/series
+++ b/debian/patches/series
@@ -3,3 +3,4 @@
0003-Fix-non-exhaustive-pattern-matching-in-jc_annot_infe.patch
0004-Default-to-why2-for-jessie-atp.patch
0005-Fix-Jc_annot_inference-use-old_reg_pos.patch
+0006-Fix-spelling-error-in-binary.patch
diff --git a/src/smtlib.ml b/src/smtlib.ml
index 3dcfe16..7c99f9d 100644
--- a/src/smtlib.ml
+++ b/src/smtlib.ml
@@ -311,7 +311,7 @@ let print_obligation fmt loc _is_lemma _o s =
fprintf fmt "@]@\n@\n"
(*
- useless since goals are split
+ useless since goals are splitted
(moreover, may trigger a bug with Z3: proves the lemma using the aussmption
given after)
if is_lemma then begin
diff --git a/tools/dp.ml b/tools/dp.ml
index b672d8e..c09f436 100644
--- a/tools/dp.ml
+++ b/tools/dp.ml
@@ -72,7 +72,7 @@ let spec =
"-select", Arg.Set select_hypotheses,
"applies some selection of hypotheses (only Alt-Ergo)";
"-simple", Arg.Set simple, "Print only Valid, I don't know, Invalid, Fail,
Timeout";
- "-split", Arg.Set split, "Create a directory wich contains all the goal
split in different file";
+ "-split", Arg.Set split, "Create a directory wich contains all the goal
splitted in different file";
"-prover", Arg.Symbol (
["Alt-Ergo";"CVC3";"CVCL";"Z3";"Yices";"Simplify";"Vampire";
"VeriT"],(fun s -> prover := Some s)), "Select the prover to use"
]
--
why packaging
_______________________________________________
Pkg-ocaml-maint-commits mailing list
Pkg-ocaml-maint-commits@lists.alioth.debian.org
http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/pkg-ocaml-maint-commits
