diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2023-02-20 10:28:37 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2023-02-20 10:28:37 +0100 |
| commit | e306714815c33121ee165b5e8825ca1c8187fc96 (patch) | |
| tree | f971b2e1e289b89f4e46547a4b2f2a9c5bace183 | |
| parent | 9d06ed97f493f89ab41f1dc3962840eadacd3865 (diff) | |
| download | compcert-e306714815c33121ee165b5e8825ca1c8187fc96.tar.gz compcert-e306714815c33121ee165b5e8825ca1c8187fc96.zip | |
When installing the Coq development, also install coq-native generated files
If the Coq version used supports native compilation, `.coq-native`
directories are generated during the build, and they need to be
installed along the `.vo` files.
Fixes: #476
| -rw-r--r-- | Makefile | 7 |
1 files changed, 6 insertions, 1 deletions
@@ -326,8 +326,13 @@ endif ifeq ($(INSTALL_COQDEV),true) install -d $(DESTDIR)$(COQDEVDIR) for d in $(DIRS); do \ - install -d $(DESTDIR)$(COQDEVDIR)/$$d && \ + set -e; \ + install -d $(DESTDIR)$(COQDEVDIR)/$$d; \ install -m 0644 $$d/*.vo $(DESTDIR)$(COQDEVDIR)/$$d/; \ + if test -d $$d/.coq-native; then \ + install -d $(DESTDIR)$(COQDEVDIR)/$$d/.coq-native; \ + install -m 0644 $$d/.coq-native/* $(DESTDIR)$(COQDEVDIR)/$$d/.coq-native/; \ + fi \ done install -m 0644 ./VERSION $(DESTDIR)$(COQDEVDIR) install -m 0644 ./compcert.config $(DESTDIR)$(COQDEVDIR) |