aboutsummaryrefslogtreecommitdiff
path: root/dev/doc/xml-protocol.md
diff options
context:
space:
mode:
authorThéo Zimmermann2019-05-22 17:38:06 +0200
committerThéo Zimmermann2019-05-22 17:38:06 +0200
commit049cfe725d334fb863df31ee9e03db4b54a64455 (patch)
tree2149121e604d2b369eb001289bf64adf508afc21 /dev/doc/xml-protocol.md
parented7d118e8ee9a6725daafde31845981f5da8d2b4 (diff)
parent0001b6d108c2d2c058b0bfca7e0af888c026fe05 (diff)
Merge PR #10203: Fixing typos - Part 1
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: cpitclaudel Reviewed-by: gares Reviewed-by: jfehrle Reviewed-by: vbgl
Diffstat (limited to 'dev/doc/xml-protocol.md')
-rw-r--r--dev/doc/xml-protocol.md2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/doc/xml-protocol.md b/dev/doc/xml-protocol.md
index 48671c03b6..e23d1234f7 100644
--- a/dev/doc/xml-protocol.md
+++ b/dev/doc/xml-protocol.md
@@ -437,7 +437,7 @@ Searches for objects that satisfy a list of constraints. If `${positiveConstrain
* Type pattern: `${constraintType} = "type_pattern"`; `${constraintValue}` is a pattern (???: an open gallina term) string.
* SubType pattern: `${constraintType} = "subtype_pattern"`; `${constraintValue}` is a pattern (???: an open gallina term) string.
* In module: `${constraintType} = "in_module"`; `${constraintValue}` is a list of strings specifying the module/directory structure.
-* Include blacklist: `${constraintType} = "include_blacklist"`; `${constraintValue}` *is ommitted*.
+* Include blacklist: `${constraintType} = "include_blacklist"`; `${constraintValue}` *is omitted*.
-------------------------------