From 1c8281a6e99f8bc21bcebb8b7a861b51bfec292e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Wed, 21 Apr 2021 22:50:21 +0200
Subject: [PATCH] Fix instructions in README and lint Colibrics opam file

---
 README.md      | 2 +-
 colibrics.opam | 5 +++++
 dune-project   | 4 ++++
 3 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 9d20f7fb9..95a352347 100644
--- a/README.md
+++ b/README.md
@@ -8,7 +8,7 @@ COLIBRICS written in Eclipse Prolog by Bruno Marre
 Using [opam](http://opam.ocaml.org/):
 
 ```shell
-opam pin add colibri2  https://git.frama-c.com/bobot/colibri2.git
+opam pin add https://git.frama-c.com/bobot/colibri2.git
 ```
 
 ## Development ##
diff --git a/colibrics.opam b/colibrics.opam
index 09cd7ff21..8df0d602d 100644
--- a/colibrics.opam
+++ b/colibrics.opam
@@ -1,5 +1,10 @@
 # This file is generated by dune, edit dune-project instead
 opam-version: "2.0"
+synopsis: "A CP solver proved in Why3"
+description:
+  "The core of Colibrics is formally proved using Why3. It offers also libraries that define formally proved simple propagation domains "
+maintainer: ["François Bobot"]
+authors: ["François Bobot"]
 homepage: "https://git.frama-c.com/bobot/colibrics"
 bug-reports: "https://git.frama-c.com/bobot/colibrics/issues"
 depends: [
diff --git a/dune-project b/dune-project
index 65842d36c..d012b637e 100644
--- a/dune-project
+++ b/dune-project
@@ -6,6 +6,10 @@
 (name colibrics)
 (package
   (name colibrics)
+  (authors "François Bobot")
+  (maintainers "François Bobot")
+  (synopsis "A CP solver proved in Why3")
+  (description "The core of Colibrics is formally proved using Why3. It offers also libraries that define formally proved simple propagation domains ")
   (depends
     "ppx_deriving_yojson"
     ("dolmen" (>= "0.5~dev"))
-- 
GitLab