diff options
author | Jason Gross <jgross@mit.edu> | 2018-07-16 09:28:56 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-07-16 09:29:17 -0400 |
commit | 6bf19130203c83bb72dd20a5c1ccd99a6716cb3b (patch) | |
tree | 3ae04926b71e64e0db99ff2897501ac04980b0aa /vernac/himsg.ml | |
parent | e27d2fd32e40937e48889772361f1cf53dd9c48e (diff) |
Only check overlay extensions on git-tracked files
This way, when editors leave over temporary files from editing
user-overlays, we don't prevent commits unless they are added to git.
Diffstat (limited to 'vernac/himsg.ml')
0 files changed, 0 insertions, 0 deletions