diff options
| author | Théo Zimmermann | 2020-06-05 13:05:08 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-06-05 13:36:58 +0200 |
| commit | 4f4ad5678db3e7aaf42f14d6d2d9000550c5f826 (patch) | |
| tree | 4bf0c6f1f89f2cd5b804b79bdb60022df73d9bfd /kernel/genOpcodeFiles.ml | |
| parent | db768e6828af62e06eb03d36509be6f8fc1efbf3 (diff) | |
Fix version switcher when building with Dune.
Closes #12395.
Diffstat (limited to 'kernel/genOpcodeFiles.ml')
0 files changed, 0 insertions, 0 deletions