diff options
-rw-r--r-- | CHANGES.log | 2 | ||||
-rw-r--r-- | doc/gh-pages.sh | 15 | ||||
-rw-r--r-- | logbook.opam | 9 |
3 files changed, 10 insertions, 16 deletions
diff --git a/CHANGES.log b/CHANGES.log index fb872ad..873e9fe 100644 --- a/CHANGES.log +++ b/CHANGES.log @@ -1,4 +1,4 @@ -[2020-05-19] +[2020-05-20] v0.3 + Compatibility with newer dependencies diff --git a/doc/gh-pages.sh b/doc/gh-pages.sh deleted file mode 100644 index 9a5bcec..0000000 --- a/doc/gh-pages.sh +++ /dev/null @@ -1,15 +0,0 @@ -#!/bin/sh -set -e - -REV=$(git rev-parse HEAD) - -cd "$(dirname "$0")" -git stash -dune build @doc -git checkout gh-pages -rm -rf doc -cp -R _build/default/_doc/_html doc -git add doc -git commit -m "Update documentation for $REV" -git checkout master -git stash apply diff --git a/logbook.opam b/logbook.opam index a115bf1..0b1632c 100644 --- a/logbook.opam +++ b/logbook.opam @@ -3,6 +3,15 @@ maintainer: "sternenseemann <post@lukasepple.de>" authors: ["sternenseemann <post@lukasepple.de>"] homepage: "https://github.com/sternenseemann/logbook" doc: "https://sternenseemann.github.io/logbook/doc" +synopsis: "A tool for keeping a personal log" +description: """ +logbook is a tool for generating HTML renderings of +log files, a file format for a personal log/diary. +By restricting who may access what parts of entries +renderings can be shared without leaking private +information. This package also includes a module +Log for parsing and manipulating log files. +""" license: "ISC" dev-repo: "https://github.com/sternenseemann/logbook.git" bug-reports: "https://github.com/sternenseemann/logbook/issues" |