diff options
Diffstat (limited to 'tools/coqwc.mll')
| -rw-r--r-- | tools/coqwc.mll | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqwc.mll b/tools/coqwc.mll index f0f138740c..06b4ad5fd3 100644 --- a/tools/coqwc.mll +++ b/tools/coqwc.mll @@ -207,7 +207,7 @@ and string = parse | eof { 0 } (*s The following entry [read_header] is used to skip the possible header at - the beggining of files (unless option \texttt{-e} is specified). + the beginning of files (unless option \texttt{-e} is specified). It stops whenever it encounters an empty line or any character outside a comment. In this last case, it correctly resets the lexer position on that character (decreasing [lex_curr_pos] by 1). *) |