aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Andres Erbsen <andreser@mit.edu>2016-02-28 16:31:08 -0500
committerGravatar Andres Erbsen <andreser@mit.edu>2016-02-28 16:56:08 -0500
commit63af66f190350b1fdfe9f905eb88d996a23f68a9 (patch)
treec613e245afb55c68b732dc31e739e0b4cb5c5ab1 /Makefile
parentc3c409f8fb014273fb8049aeb8b171390f18022f (diff)
Makefile: single-quotes for shell globbing
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
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