diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-02-28 16:31:08 -0500 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-02-28 16:56:08 -0500 |
commit | 63af66f190350b1fdfe9f905eb88d996a23f68a9 (patch) | |
tree | c613e245afb55c68b732dc31e739e0b4cb5c5ab1 /Makefile | |
parent | c3c409f8fb014273fb8049aeb8b171390f18022f (diff) |
Makefile: single-quotes for shell globbing
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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 |