From a2a249211c2ac1e18eff0d4f28e5afc98c137f97 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 5 May 2014 14:05:12 -0400
Subject: Fix install target in Makefile after
 6acf543800fe176ca7d47ef7165ebc14588efb6f.

Should decrease the noise level in the bench.
---
 Makefile.common | 4 ++--
 1 file 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))
 
-- 
cgit v1.2.3