diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-07 00:34:22 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-07 00:34:22 -0400 |
| commit | e7a7d97ff871d672b60a8f7e1ed73b9e263e121c (patch) | |
| tree | 9e3ef36f90a1e4e0fab20d9894584cdf9a76a4d4 /Makefile | |
| parent | b9cef258a2dcfcc0fa09c5e4c98b8f2928485f6c (diff) | |
Don't duplicate entries when updating _CoqProject
This can happen if you're in the middle of resolving a merge conflict (git ls-files will list some files twice).
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -14,7 +14,7 @@ HIDE := $(if $(VERBOSE),,@) install-coqprime clean-coqprime coqprime \ specific non-specific -SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g' +SORT_COQPROJECT = sed 's,[^/]*/,~&,g' | env LC_COLLATE=C sort | sed 's,~,,g' | uniq FAST_TARGETS += archclean clean cleanall clean-coqprime printenv clean-old update-_CoqProject Makefile.coq SUPER_FAST_TARGETS += update-_CoqProject Makefile.coq |