From 63af66f190350b1fdfe9f905eb88d996a23f68a9 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andreser@mit.edu>
Date: Sun, 28 Feb 2016 16:31:08 -0500
Subject: Makefile: single-quotes for shell globbing

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 2fc573520..890d2384e 100644
--- a/Makefile
+++ b/Makefile
@@ -7,7 +7,7 @@ SRC_DIR  := src
 SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g'
 
 update-_CoqProject::
-	(echo '-R $(SRC_DIR) $(MOD_NAME)'; (git ls-files "src/*.v" | $(SORT_COQPROJECT))) > _CoqProject
+	(echo '-R $(SRC_DIR) $(MOD_NAME)'; (git ls-files 'src/*.v' | $(SORT_COQPROJECT))) > _CoqProject
 
 coq: coqprime Makefile.coq
 	$(MAKE) -f Makefile.coq
-- 
cgit v1.2.3