OPAM/OCaml scripts for CI

install_opam.sh

#!/usr/bin/env sh -xeu

##
## Usage:
##   curl -sL https://gist.githubusercontent.com/akabe/24979afbf95c4cf4393f589cda997e1b/raw/install_opam.sh | sh -xeu
##
## Variables:
## - $OPAM_PREFIX     Path to install opam
## - $OPAM_VERSION    Version of OPAM to be installed
## - $OCAML_VERSION   Version of OCaml to be installed
## - $OPAM_INIT_FLAGS Parameters passing to `opam init'
##

if ! which opam; then
  mkdir -p "$OPAM_PREFIX/bin"
  curl "https://github.com/ocaml/opam/releases/download/$OPAM_VERSION/opam-$OPAM_VERSION-$(uname -m)-$(uname -s)" \
       -Lo "$OPAM_PREFIX/bin/opam"
  chmod 755 "$OPAM_PREFIX/bin/opam"
  opam init -a -y --comp "$OCAML_VERSION" ${OPAM_INIT_FLAGS:-}
fi

update_gh-pages_jbuilder.sh

#!/usr/bin/env sh -exu

##
## Usage: https://gist.githubusercontent.com/akabe/24979afbf95c4cf4393f589cda997e1b/raw/update-gh-pages-dune.sh | sh -xeu _build/default/lib
##
## Variables:
## - $GIT_REMOTE_URL       URL to git remote repository where you can push to.
## - $TRAVIS_BRANCH        Defined by Travis CI
## - $TRAVIS_PULL_REQUEST  Defined by Travis CI
##

if [ "${GIT_REMOTE_URL:-}" == '' ]; then
  echo "[SKIPPED] \$GIT_REMOTE_URL is empty or undefined."
elif [ "$TRAVIS_BRANCH" != 'master' ]; then
  echo "[SKIPPED] This is not master branch: \$TRAVIS_BRANCH = $TRAVIS_BRANCH"
elif [ "$TRAVIS_PULL_REQUEST" == 'true' ]; then
  echo "[SKIPPED] This is a pull request: \$TRAVIS_PULL_REQUEST = $TRAVIS_PULL_REQUEST"
else
  opam install -y odoc
  if which dune >/dev/null; then
    dune subst
    dune build @doc
    html_dir=_build/default/_doc
  else
    dune subst
    dune build @doc
    html_dir=_build/default/_doc/_html
  fi

  if git clone "$GIT_REMOTE_URL" -b gh-pages gh-pages; then # `gh-pages' branch already exists.
    rm -rf gh-pages/*.md gh-pages/api
  else # Creates orphan `gh-pages' branch.
    mkdir gh-pages
    ( cd gh-pages
      git init
      git checkout --orphan gh-pages
      git remote add origin "$GIT_REMOTE_URL" )
  fi

  cp *.md gh-pages/
  cp -r "$html_dir" gh-pages/api

  ( cd gh-pages
    git add *.md api
    git -c user.name='TravisCI' -c user.email='travis-ci@example.com' commit -m 'Update documentation'
    git push origin gh-pages )
fi