diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2020-04-17 17:26:15 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2020-04-27 09:57:40 +0200 |
| commit | 64fe7f462c4dd204ac5ffaed48edbf9698485d94 (patch) | |
| tree | 6e2b3cdb5a7d13ebd00ba242bc5e690982f2f703 /Makefile | |
| parent | 438d541dbe5fe7d7fe6b7aacaa6e6ef070c2e237 (diff) | |
| download | compcert-64fe7f462c4dd204ac5ffaed48edbf9698485d94.tar.gz compcert-64fe7f462c4dd204ac5ffaed48edbf9698485d94.zip | |
Simplify the generation of driver/Version.ml
Don't use sed, just echo the contents of the file.
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 11 |
1 files changed, 8 insertions, 3 deletions
@@ -14,6 +14,11 @@ ####################################################################### include Makefile.config +include VERSION + +BUILDVERSION ?= $(version) +BUILDNR ?= $(buildnr) +TAG ?= $(tag) ifeq ($(wildcard $(ARCH)_$(BITSIZE)),) ARCHDIRS=$(ARCH) @@ -220,9 +225,9 @@ compcert.ini: Makefile.config > compcert.ini driver/Version.ml: VERSION - cat VERSION \ - | sed -e 's|\(.*\)=\(.*\)|let \1 = \"\2\"|g' \ - >driver/Version.ml + (echo 'let version = "$(BUILDVERSION)"'; \ + echo 'let buildnr = "$(BUILDNR)"'; \ + echo 'let tag = "$(TAG)"';) > driver/Version.ml cparser/Parser.v: cparser/Parser.vy @rm -f $@ |