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 /src/Util/Tactics | |
| 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 'src/Util/Tactics')
0 files changed, 0 insertions, 0 deletions