diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/doc/changes.txt | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index d52c184623..0b0c0f5bfb 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -162,7 +162,7 @@ uses type classes and rejects terms with unresolved holes. functions that used to carry a suffix `_loc`, such suffix has been dropped. -- `errorlabstrm` has been removed in favor of `user_err`. +- `errorlabstrm` and `error` has been removed in favor of `user_err`. - The header parameter to `user_err` has been made optional. |