1 #!/usr/bin/env bash 2 # Build the odoc HTML documentation and open it in a browser. 3 # 4 # scripts/docs.sh build, then open 5 # scripts/docs.sh --print build, then print the entry point path 6 # 7 # Equivalent to `dune build @doc`; this wrapper exists only to locate the entry 8 # point, which is buried in the build directory. 9 10 set -euo pipefail 11 12 root=$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd) 13 cd "$root" 14 15 entry="_build/default/_doc/_html/index.html" 16 17 opam exec -- dune build @doc 18 19 if [[ ! -f $entry ]]; then 20 printf 'error: expected documentation at %s\n' "$entry" >&2 21 exit 1 22 fi 23 24 if [[ ${1-} == --print ]]; then 25 printf '%s/%s\n' "$root" "$entry" 26 exit 0 27 fi 28 29 url="file://$root/$entry" 30 31 # xdg-open detaches, so suppress the browser's own chatter on stderr. 32 if command -v xdg-open > /dev/null; then 33 xdg-open "$url" > /dev/null 2>&1 & 34 printf 'opened %s\n' "$url" 35 else 36 printf 'no xdg-open found; open this manually:\n%s\n' "$url" 37 fi 38