aboutsummaryrefslogtreecommitdiff
path: root/kernel/cbytecodes.ml
diff options
context:
space:
mode:
authorHugo Herbelin2020-04-30 21:13:18 +0200
committerHugo Herbelin2020-05-10 00:09:49 +0200
commit01e465952e79f4e7fdef3417c6f1883ca2c5e328 (patch)
treebbb9625200e9a30b6bed9aabef9e9c0f3c182091 /kernel/cbytecodes.ml
parent2760d13b4bc70738cf10f1e6864764f62dcef32d (diff)
Locating error again in TacAtom and TacAlias (fixes #12152, fixes #12255).
Since we don't always have the call trace anymore, we explicitly insert a catch of failures in TacAlias. The trace is then treated in this catch rather than propagated to the underlying calls (a VFun?). I hope this is doing the same. The suggestion to use a tclOR is from P.-M. Pédrot. Note: this is not fully ideal, the messages which were expecting a trace should be rethought to take into account either that the calls are not printed anymore, or to print them again.
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions