From 93f9638a1b84fd97c62904816228b1c11573eb55 Mon Sep 17 00:00:00 2001 From: Leo Alt Date: Tue, 10 May 2022 19:05:14 +0200 Subject: [PATCH] Add error id to script --- scripts/error_codes.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/error_codes.py b/scripts/error_codes.py index f3d35cae4..84ba08bc0 100755 --- a/scripts/error_codes.py +++ b/scripts/error_codes.py @@ -232,7 +232,7 @@ def examine_id_coverage(top_dir, source_id_to_file_names, new_ids_only=False): "3893", "3996", "4010", "4802", "5272", "5622", "7128", "7400", "7589", "7593", "7649", "7710", - "8065", "8084", "8140", + "8065", "8084", "8140", "8158", "8312", "8592", "9134", "9609", }