aboutsummaryrefslogtreecommitdiff
path: root/tools/dune
diff options
context:
space:
mode:
authorChimrod <>2023-10-03 08:44:15 +0200
committerChimrod <>2023-10-03 08:49:36 +0200
commite8b746742fdeb44ea976d867001c7b0815df1543 (patch)
tree08572e79f94b5d8332b7484078cb381cf0d3e2f5 /tools/dune
parentea509dd21ebec0ecb4f307d9786ca75dc03eab75 (diff)
Update the compilation rule for git hash inclusion
Diffstat (limited to 'tools/dune')
-rw-r--r--tools/dune2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/dune b/tools/dune
index 2e223d4..29ee744 100644
--- a/tools/dune
+++ b/tools/dune
@@ -3,7 +3,7 @@
(rule
(target git_hash.ml)
- (deps git_head.sh)
+ (deps git_head.sh (universe))
(action
(with-stdout-to
%{target}