diff options
| author | Maxime Dénès | 2014-05-05 14:05:12 -0400 |
|---|---|---|
| committer | Maxime Dénès | 2014-05-05 14:05:12 -0400 |
| commit | a2a249211c2ac1e18eff0d4f28e5afc98c137f97 (patch) | |
| tree | f426e3d9befe93ebfc24d00a37c11d6953068099 | |
| parent | 1432318faa4cb6a50eca2c7a371b43b3b9969666 (diff) | |
Fix install target in Makefile after 6acf543800fe176ca7d47ef7165ebc14588efb6f.
Should decrease the noise level in the bench.
| -rw-r--r-- | Makefile.common | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.common b/Makefile.common index d45c1d5614..d971e9b2eb 100644 --- a/Makefile.common +++ b/Makefile.common @@ -324,9 +324,9 @@ vo_to_mod = $(subst /,.,$(patsubst theories/%,Coq.%,$(patsubst plugins/%,Coq.%,$ # Converting a stdlib filename into native compiler filenames # Used for install targets -vo_to_cm = $(foreach vo,$(1),$(dir $(vo))$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.cm*))))) +vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.cm*))))) -vo_to_obj = $(foreach vo,$(1),$(dir $(vo))$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o))))) +vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.vo=.o))))) ALLMODS:=$(call vo_to_mod,$(ALLVO)) |