Commit 63256102 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Put the git commit in the cduce version string.

parent f4b661e6
......@@ -36,8 +36,12 @@ else
GIT_COMMIT=$(shell test -x "$$(which git)" && git rev-parse --short HEAD)
GIT_VERSION=$(subst -devel,-devel-$(GIT_COMMIT),$(VERSION))
SYNTAX = -I misc/ q_symbol.cmo \
-symbol cduce_version=\"$(VERSION)\" \
-symbol cduce_version=\"$(GIT_VERSION)\" \
-symbol build_date=\"$(shell date +%Y-%m-%d)\" \
-symbol session_dir=\"$(SESSION_DIR)\" \
-loc "_loc"
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment