[Pkg-ocaml-maint-commits] [SCM] why packaging branch, master, updated. debian/2.13-1-43-g47ec9e8

Mehdi Dogguy dogguy at pps.jussieu.fr
Wed Dec 17 18:30:34 UTC 2008


The following commit has been merged in the master branch:
commit 32fc4aa328e87cde8a4f8d6a52922b860fcd0c8b
Author: Mehdi Dogguy <dogguy at pps.jussieu.fr>
Date:   Wed Dec 17 19:29:09 2008 +0100

    Adding a new binary package why-examples

diff --git a/debian/control b/debian/control
index f193219..8fe3dc7 100644
--- a/debian/control
+++ b/debian/control
@@ -20,6 +20,17 @@ Description: A software verification tool
  assistants Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar and the
  decision procedures Simplify, Ergo, Yices, CVC Lite and haRVey.
 
+Package: why-examples
+Architecture: all
+Section: doc
+Description: Examples of programs certified with Why
+ Why aims at being a verification conditions generator (VCG) back-end
+ for other verification tools. It provides a powerful input language
+ including higher-order functions, polymorphism, references, arrays and
+ exceptions. It generates proof obligations for many systems: the proof
+ assistants Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar and the
+ decision procedures Simplify, Ergo, Yices, CVC Lite and haRVey.
+
 Package: libjessie-ocaml-dev
 Architecture: any
 Depends: ocaml-nox-${F:OCamlABI}
diff --git a/debian/why-examples.install b/debian/why-examples.install
new file mode 100644
index 0000000..2e87d17
--- /dev/null
+++ b/debian/why-examples.install
@@ -0,0 +1,2 @@
+examples-c/ usr/share/doc/why/
+examples/ usr/share/doc/why/

-- 
why packaging



More information about the Pkg-ocaml-maint-commits mailing list