Dune fix

PLTools · Nov 15, 2024 · 751f556 · 751f556
1 parent 0981047
commit 751f556
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/src/dune b/src/dune
@@ -11,11 +11,11 @@
     version2.ml
     (progn
      (run echo let version = "\"")
-     (run echo Version)
+     (run echo "Version ")
      (run git rev-parse --abbrev-ref HEAD)
-     (run echo , " ")
+     (run echo ", ")
      (run git rev-parse --short HEAD)
-     (run echo , " ")
+     (run echo ", ")
      (pipe-stdout
       (run git rev-parse --verify HEAD)
       (run git show --no-patch --no-notes --pretty='%cd'))