in lean/scripts/lint_style.py [0:0]
def output_message(path, line_nr, code, msg):
if len(exceptions) == 0:
# we are generating a new exceptions file
# filename first, then line so that we can call "sort" on the output
print(f"{path} : line {line_nr} : {code} : {msg}")
else:
# We are outputting for github. It doesn't appear to surface code, so show it in the message too
print(f"::error file={path},line={line_nr},code={code}::{code}: {msg}")