diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-04-05 10:19:01 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-04-06 13:19:31 +0200 |
commit | 217b20d9abb5e079e6ef7fed06dada5332d558fe (patch) | |
tree | 597b27d7b28630f9aa5c6a8dbee5389b53ccc599 /dev/ci/user-overlays/06745-ejgallego-located+vernac.sh | |
parent | f95d33479cae45a5f6f18eb260e3c9ffcb605882 (diff) |
Fix #6956: Uncaught exception in bytecode compilation
We also make the code of [compact] in kernel/univ.ml a bit clearer.
Diffstat (limited to 'dev/ci/user-overlays/06745-ejgallego-located+vernac.sh')
0 files changed, 0 insertions, 0 deletions