diff options
| author | Hugo Herbelin | 2020-04-30 21:13:18 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-10 00:09:49 +0200 |
| commit | 01e465952e79f4e7fdef3417c6f1883ca2c5e328 (patch) | |
| tree | bbb9625200e9a30b6bed9aabef9e9c0f3c182091 /kernel/cbytecodes.ml | |
| parent | 2760d13b4bc70738cf10f1e6864764f62dcef32d (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
