diff options
author | Chimrod <> | 2023-10-03 08:44:15 +0200 |
---|---|---|
committer | Chimrod <> | 2023-10-03 08:49:36 +0200 |
commit | e8b746742fdeb44ea976d867001c7b0815df1543 (patch) | |
tree | 08572e79f94b5d8332b7484078cb381cf0d3e2f5 /tools | |
parent | ea509dd21ebec0ecb4f307d9786ca75dc03eab75 (diff) |
Update the compilation rule for git hash inclusion
Diffstat (limited to 'tools')
-rw-r--r-- | tools/dune | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -3,7 +3,7 @@ (rule (target git_hash.ml) - (deps git_head.sh) + (deps git_head.sh (universe)) (action (with-stdout-to %{target} |