diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-29 17:47:06 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-12 16:49:46 +0200 |
| commit | 2f0a56562112c4bd66082fb3eafffb8cf6f03a88 (patch) | |
| tree | 2586dcdbe566519fa5325fa2551f658fbb87a700 /dev/doc/unification.txt | |
| parent | 55bddb4bf35fa68318aa57a5fa8a113d1fe51159 (diff) | |
[stm] Improve error messages on add/parse.
As suggested by @psteckler in #524 , we give more explicit information
about what is wrong.
We also provide some debug information for the possible dangerous case
of having the tip go out of sync with the real installed state (which
will make parsing fail if there was some changes to the parser).
We also fix a couple of typos noticed by Paul, thanks Paul.
Diffstat (limited to 'dev/doc/unification.txt')
0 files changed, 0 insertions, 0 deletions