aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-07-16 16:29:22 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-07-16 16:29:22 +0200
commitb799252775563b4f46f5ea39cbfc469759e7a296 (patch)
tree3ae04926b71e64e0db99ff2897501ac04980b0aa /theories
parente27d2fd32e40937e48889772361f1cf53dd9c48e (diff)
parent6bf19130203c83bb72dd20a5c1ccd99a6716cb3b (diff)
Merge PR #8069: Only check overlay extensions on git-tracked files
Diffstat (limited to 'theories')
0 files changed, 0 insertions, 0 deletions