diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-com.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 1bd3d148e2..5a3c91404b 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -308,7 +308,7 @@ of all these libraries is then type-checked. The effect of {\tt and with positive exit code if an error has been found. Error messages are not deemed to help the user understand what is wrong. In the current version, it does not modify the compiled libraries to mark -them as succesfully checked. +them as successfully checked. Note that non-logical information is not checked. By logical information, we mean the type and optional body associated to names. |