fix(lint-style.py): do not barf on new copyright exceptions (#15833)

grunweg · grunweg · commit 3e38319ac0bf · 2024-08-15T12:19:31.000Z
diff --git a/scripts/lint-style.py b/scripts/lint-style.py
@@ -61,7 +61,7 @@
         path = ROOT_DIR / filename
         if errno == "ERR_MOD":
             exceptions += [(ERR_MOD, path, None)]
-        elif errno in ["ERR_LIN", "ERR_ADN", "ERR_NUM_LIN"]:
+        elif errno in ["ERR_COP", "ERR_LIN", "ERR_ADN", "ERR_NUM_LIN"]:
             pass # maintained by the Lean style linter now
         else:
             print(f"Error: unexpected errno in style-exceptions.txt: {errno}")
