diff options
| author | Hugo Herbelin | 2018-07-25 17:29:16 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-07-25 17:29:16 +0200 |
| commit | 6f52f7bce0de9ac58142b05e17b5dc380fc169e7 (patch) | |
| tree | 7357f0850eb60fe532fce4831910f1896af5c078 /plugins | |
| parent | 523de4f878293cf1d582bd70300b34d497e705b3 (diff) | |
Doc: preliminary work before #7291 which add an "Unable to unify" message.
We adopt the convention that error messages with a template use the
sphinx syntax used in defining syntax rules.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions