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 /plugins/fourier/fourier.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 'plugins/fourier/fourier.ml')
0 files changed, 0 insertions, 0 deletions