diff options
| author | Gaëtan Gilbert | 2020-10-19 14:53:40 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-10-19 16:13:13 +0200 |
| commit | 65f32dfa52f51d59581368aafbf18832d276977c (patch) | |
| tree | 02ca1c324e866e86077408307037f58cdb59e41b /kernel/vmbytecodes.mli | |
| parent | 33f6551fd030643d0accf50dd762bcede5dd4b8b (diff) | |
Bench: move variables to the script
IMO it makes more sense this way, also it's more convenient if someone
wants to run the script locally.
Diffstat (limited to 'kernel/vmbytecodes.mli')
0 files changed, 0 insertions, 0 deletions