aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorscinart2019-10-27 23:05:13 -0400
committerscinart2019-10-27 23:20:38 -0400
commit5d143285677704a406b059aba392a5cf304c67d6 (patch)
tree95a96a512b4b9634f0464bbfd937dee65e9529ed
parent943dcfec49b38267488e01cc680fa456739b92cc (diff)
Remove the incorrect extra space in Makefile.vofiles
Which results in extra space in filenames when compiling.
-rw-r--r--Makefile.vofiles4
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.vofiles b/Makefile.vofiles
index 5296ed43ff..4eb0a170ed 100644
--- a/Makefile.vofiles
+++ b/Makefile.vofiles
@@ -31,9 +31,9 @@ ALLMODS:=$(call vo_to_mod,$(ALLVO:.$(VO)=.vo))
# Converting a stdlib filename into native compiler filenames
# Used for install targets
-vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst user-contrib/%, N%, $(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.cm*))))))
+vo_to_cm = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst user-contrib/%,N%, $(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.cm*))))))
-vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst user-contrib/%, N%, $(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.o))))))
+vo_to_obj = $(foreach vo,$(1),$(dir $(vo)).coq-native/$(subst /,_,$(patsubst user-contrib/%,N%, $(patsubst theories/%,NCoq_%,$(patsubst plugins/%,NCoq_%,$(vo:.$(VO)=.o))))))
ifdef QUICK
GLOBFILES:=