diff options
| author | Théo Zimmermann | 2019-07-16 08:59:04 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-07-16 08:59:04 +0200 |
| commit | ba1bb7581a5ad0969d35911fffdf61f150e0536f (patch) | |
| tree | 0dd7fd842abaaa9b0168f418498b8adf411c3401 /dev/doc | |
| parent | a5998b06ccf2367f7d1e58dc80e4237754c953bc (diff) | |
| parent | 93032fc1b900b603d52376e1841ad1c590ae4da5 (diff) | |
Merge PR #10520: Fix typos
Reviewed-by: Zimmi48
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/xml-protocol.md | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md index e23d1234f7..a3e1a4e90b 100644 --- a/dev/doc/xml-protocol.md +++ b/dev/doc/xml-protocol.md @@ -174,7 +174,7 @@ Moves current tip to `${stateId}`, such that commands may be added to the new st </union> </value> ``` -* Failure: If `stateId` is in an error-state and cannot be jumped to, `errorFreeStateId` is the parent state of ``stateId` that shopuld be edited instead. +* Failure: If `stateId` is in an error-state and cannot be jumped to, `errorFreeStateId` is the parent state of `stateId` that should be edited instead. ```html <value val="fail" loc_s="${startOffsetOfError}" loc_e="${endOffsetOfError}"> <state_id val="${errorFreeStateId}"/> |
