diff --git a/docs/commandref.html b/docs/commandref.html index b968348aa..c852e26ed 100644 --- a/docs/commandref.html +++ b/docs/commandref.html @@ -2626,7 +2626,8 @@ A line ending with \ will be concatenated with the next one, so long lines

HOL