aboutsummaryrefslogtreecommitdiff
path: root/lib/tools
diff options
context:
space:
mode:
Diffstat (limited to 'lib/tools')
-rw-r--r--lib/tools/dune10
-rwxr-xr-xlib/tools/git_head.sh11
2 files changed, 21 insertions, 0 deletions
diff --git a/lib/tools/dune b/lib/tools/dune
new file mode 100644
index 0000000..29ee744
--- /dev/null
+++ b/lib/tools/dune
@@ -0,0 +1,10 @@
+(library
+ (name tools))
+
+(rule
+ (target git_hash.ml)
+ (deps git_head.sh (universe))
+ (action
+ (with-stdout-to
+ %{target}
+ (bash "./git_head.sh"))))
diff --git a/lib/tools/git_head.sh b/lib/tools/git_head.sh
new file mode 100755
index 0000000..bfa738a
--- /dev/null
+++ b/lib/tools/git_head.sh
@@ -0,0 +1,11 @@
+#! /bin/sh
+# Include the git hash in an OCaml file.
+
+git diff-index --quiet HEAD --
+if [ $? -ne 0 ]; then
+ revision=": untracked"
+else
+ revision=$(git rev-parse --short HEAD)
+fi
+compile_date=$(date +%Y/%m/%d)
+echo "let revision = \"${revision} - compiled on ${compile_date}\""