From e7a7d97ff871d672b60a8f7e1ed73b9e263e121c Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Fri, 7 Apr 2017 00:34:22 -0400
Subject: 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).
---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 51a17aa98..36c8e0034 100644
--- a/Makefile
+++ b/Makefile
@@ -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
-- 
cgit v1.2.3