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