diff options
Diffstat (limited to 'lib/pp_diff.mli')
| -rw-r--r-- | lib/pp_diff.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/pp_diff.mli b/lib/pp_diff.mli index 03468271d2..0eec18bd5a 100644 --- a/lib/pp_diff.mli +++ b/lib/pp_diff.mli @@ -88,7 +88,7 @@ Ppcmd_strings will be split into multiple Ppcmd_strings if a diff starts or ends in the middle of the string. Whitespace just before or just after a diff will not be part of the highlight. -Prexisting tags in pp may contain only a single Ppcmd_string. Those tags will be +Preexisting tags in pp may contain only a single Ppcmd_string. Those tags will be placed inside the diff tags to ensure proper nesting of tags within spans of "start.diff.*" ... "end.diff.*". |