diff --git a/.gitignore b/.gitignore index 85d4d798..e109d796 100644 --- a/.gitignore +++ b/.gitignore @@ -7,3 +7,6 @@ _opam *.install *.exe *.tmp +src/lib/version.ml +src/lib/.git_index_path +src/lib/.git_index.lnk diff --git a/src/lib/dune b/src/lib/dune index 78182c01..3588916b 100644 --- a/src/lib/dune +++ b/src/lib/dune @@ -1,6 +1,19 @@ +(rule + (target .git_index_path) + (deps (universe) gen_git_index_path.sh) + (action + (with-stdout-to + .git_index_path + (run sh gen_git_index_path.sh)))) + +(rule + (target .git_index.lnk) + (action + (run ln -sf %{read-lines:.git_index_path} %{target}))) + (rule (target version.ml) - (deps (universe) gen_version.sh) + (deps (file .git_index.lnk) gen_version.sh) (action (with-stdout-to version.ml diff --git a/src/lib/gen_git_index_path.sh b/src/lib/gen_git_index_path.sh new file mode 100644 index 00000000..899fbc6c --- /dev/null +++ b/src/lib/gen_git_index_path.sh @@ -0,0 +1,2 @@ +#!/bin/sh +git rev-parse --git-path index 2>/dev/null || echo /dev/null