diff options
| author | Théo Zimmermann | 2020-11-15 15:35:43 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-11-15 15:35:43 +0100 |
| commit | c02301699e9014862c52f069a130b8131fd9d692 (patch) | |
| tree | f9cba092257b65fff6c53203b0ca49fe476e865f /kernel/genOpcodeFiles.ml | |
| parent | 9a93f5836a5f7bab81384314ac11ff0aac7d1b7f (diff) | |
[ci/gitlab/windows] Do not load user overlays.
This was broken since #13177. We remove support for user overlays in
Windows build instead of fixing it since there is no specific use
case.
Diffstat (limited to 'kernel/genOpcodeFiles.ml')
0 files changed, 0 insertions, 0 deletions