diff options
| author | Benoît Viguier <ildyria@users.noreply.github.com> | 2018-05-31 17:52:12 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2018-05-31 17:52:12 +0200 |
| commit | 27ff8beb35cc4fd1e6a05c6685a7903e9e64ecdf (patch) | |
| tree | 4230e007a3f87306958a919a71f53831441ffd06 /Makefile | |
| parent | c3816c99e0464d3c8feaae9a19d3956a7acd4385 (diff) | |
| download | compcert-27ff8beb35cc4fd1e6a05c6685a7903e9e64ecdf.tar.gz compcert-27ff8beb35cc4fd1e6a05c6685a7903e9e64ecdf.zip | |
Install the VERSION file along the .vo files
This is useful for the VST project and can be useful for others.
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 1 |
1 files changed, 1 insertions, 0 deletions
@@ -259,6 +259,7 @@ ifeq ($(INSTALL_COQDEV),true) install -d $(COQDEVDIR)/$$d && \ install -m 0644 $$d/*.vo $(COQDEVDIR)/$$d/; \ done + install -m 0644 ./VERSION $(COQDEVDIR) @(echo "To use, pass the following to coq_makefile or add the following to _CoqProject:"; echo "-R $(COQDEVDIR) compcert") > $(COQDEVDIR)/README endif |