aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2016-02-25 13:46:07 -0500
committerGravatar Jason Gross <jgross@mit.edu>2016-02-25 13:46:07 -0500
commitf6733c0048eacc911feff5277fed12fb544c7299 (patch)
tree95583abe859e3e9eae68727d3642d3d8bef703d0 /Makefile
parent6dbfc76a2951a8f74b33a61f57fbe5b0d73c3352 (diff)
Factor out some bedrock dependencies into WordUtil
Also move a definition about words, with a TODO about location, into WordUtil.
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile4
1 files changed, 3 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 35cbcde24..2fc573520 100644
--- a/Makefile
+++ b/Makefile
@@ -4,8 +4,10 @@ SRC_DIR := src
.PHONY: coq clean install coqprime update-_CoqProject
.DEFAULT_GOAL := coq
+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) > _CoqProject
+ (echo '-R $(SRC_DIR) $(MOD_NAME)'; (git ls-files "src/*.v" | $(SORT_COQPROJECT))) > _CoqProject
coq: coqprime Makefile.coq
$(MAKE) -f Makefile.coq