diff options
| author | Michael Soegtrop | 2020-11-18 22:00:43 +0100 |
|---|---|---|
| committer | Michael Soegtrop | 2020-11-18 22:00:43 +0100 |
| commit | fea83b040f285e4316fd9d63d4c940d9fe444d91 (patch) | |
| tree | 8736c1e582c05846ed3604f5101ee90d5d2a9578 /interp/notation_ops.ml | |
| parent | e2f2966c453ecdf788ee1c15d62be68da2cddebe (diff) | |
| parent | c02301699e9014862c52f069a130b8131fd9d692 (diff) | |
Merge PR #13389: [ci/gitlab/windows] Do not load user overlays.
Reviewed-by: MSoegtropIMC
Diffstat (limited to 'interp/notation_ops.ml')
0 files changed, 0 insertions, 0 deletions