A RetroSearch Logo

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Search Query:

Showing content from https://github.com/agda/agda/issues/7381 below:

Our error messages do not follow the GNU standard · Issue #7381 · agda/agda · GitHub

https://www.gnu.org/prep/standards/html_node/Errors.html

Our errors look like this:

Issue3491.agda:12,23-33 
Ill-formed projection pattern .unbox
when checking that the pattern box .unbox has type Box b

The position formatting is not covered by the GNU standard, because

Valid would be e.g.

Issue3491.agda:12.23-33:
Issue3491.agda:12:23-33:

The error message can also give both the starting and ending positions of the erroneous text. There are several formats so that you can avoid redundant information such as a duplicate line number. Here are the possible formats:

sourcefile:line1.column1-line2.column2: message
sourcefile:line1.column1-column2: message

Here is the implementation of the standard for Emacs: https://github.com/emacs-mirror/emacs/blob/master/lisp/progmodes/compile.el#L416-L484


RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4