From 751f55691c0dcbfdcba97f7d083ab0537563e667 Mon Sep 17 00:00:00 2001 From: Dmitry Boulytchev Date: Fri, 15 Nov 2024 20:39:00 +0300 Subject: [PATCH] Dune fix --- src/dune | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/dune b/src/dune index 011251644..ae7211707 100644 --- 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'))