diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-07-16 16:29:22 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-07-16 16:29:22 +0200 |
| commit | b799252775563b4f46f5ea39cbfc469759e7a296 (patch) | |
| tree | 3ae04926b71e64e0db99ff2897501ac04980b0aa /pretyping/recordops.mli | |
| parent | e27d2fd32e40937e48889772361f1cf53dd9c48e (diff) | |
| parent | 6bf19130203c83bb72dd20a5c1ccd99a6716cb3b (diff) | |
Merge PR #8069: Only check overlay extensions on git-tracked files
Diffstat (limited to 'pretyping/recordops.mli')
0 files changed, 0 insertions, 0 deletions