aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-04-05 10:19:01 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-04-06 13:19:31 +0200
commit217b20d9abb5e079e6ef7fed06dada5332d558fe (patch)
tree597b27d7b28630f9aa5c6a8dbee5389b53ccc599 /dev/ci/user-overlays/06745-ejgallego-located+vernac.sh
parentf95d33479cae45a5f6f18eb260e3c9ffcb605882 (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