diff options
author | Jason Gross <jgross@mit.edu> | 2018-02-10 15:26:07 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-02-10 15:26:07 -0500 |
commit | d62ffb1a68a76cc33c502e1a8351f14104bc7ee2 (patch) | |
tree | 5513e77aad50ab3015a4a656025487d2a090194f /Makefile | |
parent | b0dca8dbd9bc959c5ccb5355e419b03714483668 (diff) |
Support older git ls-files
The older ones don't have --recurse-submodules
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -53,7 +53,7 @@ endif update-_CoqProject:: $(SHOW)'ECHO > _CoqProject' - $(HIDE)(echo '-R $(SRC_DIR) $(MOD_NAME)'; echo '-R bbv bbv'; (git ls-files --recurse-submodules 'src/*.v' 'bbv/*.v' | $(SORT_COQPROJECT))) > _CoqProject + $(HIDE)(echo '-R $(SRC_DIR) $(MOD_NAME)'; echo '-R bbv bbv'; ((git ls-files 'src/*.v'; (git submodule foreach 'git ls-files "*.v" 2>/dev/null | sed "s|^|$$path/|"' | grep 'bbv/')) | $(SORT_COQPROJECT))) > _CoqProject $(VOFILES): | coqprime |