def output_message()

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}")