Change version of menhir to $(date)

small sed command in ci-menhir.sh to change the version from "unreleased" to today's date.
Villetaneuse · Nov 11, 2023 · 56415ce · 56415ce
1 parent dece8f2
commit 56415ce
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/dev/ci/ci-menhir.sh b/dev/ci/ci-menhir.sh
@@ -10,6 +10,7 @@ git_download menhirlib
 if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
 
 ( cd "${CI_BUILD_DIR}/menhirlib"
+  sed -i.bak "s/unreleased/$(date +%Y%m%d)/" dune-project
   dune build @install -p menhirLib,menhirSdk,menhir
   dune install -p menhirLib,menhirSdk,menhir menhir menhirSdk menhirLib --prefix="$CI_INSTALL_DIR"