diff options
| author | Maxime Dénès | 2018-09-03 12:29:20 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-03 12:29:20 +0200 |
| commit | 7456164386a87df83763109e12fa8aaa71a96104 (patch) | |
| tree | d52aeec900c8cfef4fbf64a1e7750f80c8b0348e /kernel/declareops.mli | |
| parent | 03f93662a255a00a9068ef8963ab221cc62f5cfd (diff) | |
| parent | cd3040d5bb67bd17a3c4d20e3324d285657e215d (diff) | |
Merge PR #8147: [ssr] assertion -> error message (Fix #8134)
Diffstat (limited to 'kernel/declareops.mli')
0 files changed, 0 insertions, 0 deletions