diff options
| author | Maxime Dénès | 2019-01-09 17:13:41 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-09 17:13:41 +0100 |
| commit | f7d362d04d788ede814d0e090b916aa512eb8a6c (patch) | |
| tree | 70250cb0aa565f1a3efa5ff87255f0e6f4225d73 /dev/ci | |
| parent | 727d4da625f88b7ba302d5c129f9773dc1fb1e33 (diff) | |
[STM] Fix semantics of `cur_id` w.r.t. error states
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions