#!/bin/sh set -e [ "$1" = "" ] && { echo "I need the dune-project version as arg" 1>&2 exit 1 } [ "$GIT_SHA" = "" ] && GIT_SHA="$(git log -1 --format="%h")" cat <<EOF (* generated by $0 *) let dune_project_version = "$1" let git_sha = "$GIT_SHA" EOF