From b7964befd039c41c63e00ef323f9eb49061c144c Mon Sep 17 00:00:00 2001 From: Chimrod <> Date: Sun, 1 Oct 2023 19:30:58 +0200 Subject: Added the git revision in the code --- tools/dune | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 tools/dune (limited to 'tools/dune') diff --git a/tools/dune b/tools/dune new file mode 100644 index 0000000..2e223d4 --- /dev/null +++ b/tools/dune @@ -0,0 +1,10 @@ +(library + (name tools)) + +(rule + (target git_hash.ml) + (deps git_head.sh) + (action + (with-stdout-to + %{target} + (bash "./git_head.sh")))) -- cgit v1.2.3