diff --git a/.github/workflows/sync_files.yml b/.github/workflows/sync_files.yml
new file mode 100644
index 00000000000..a102f822330
--- /dev/null
+++ b/.github/workflows/sync_files.yml
@@ -0,0 +1,17 @@
+name: Check synchronized files
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+    branches: [main]
+
+jobs:
+  sync:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v2
+        with:
+          submodules: true
+      - name: Check synchronized files
+        run: scripts/sync-identical-files.py
diff --git a/.gitmodules b/.gitmodules
index e69de29bb2d..b9b6762c49b 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -0,0 +1,3 @@
+[submodule "codeql"]
+	path = codeql
+	url = https://github.com/github/codeql.git
diff --git a/codeql b/codeql
new file mode 160000
index 00000000000..fc2fe6cccb8
--- /dev/null
+++ b/codeql
@@ -0,0 +1 @@
+Subproject commit fc2fe6cccb81b7d3ec5d9746ef05b07497ceb635
diff --git a/scripts/identical-files.json b/scripts/identical-files.json
new file mode 100644
index 00000000000..9e26dfeeb6e
--- /dev/null
+++ b/scripts/identical-files.json
@@ -0,0 +1 @@
+{}
\ No newline at end of file
diff --git a/scripts/sync-identical-files.py b/scripts/sync-identical-files.py
new file mode 100755
index 00000000000..17fe22808e9
--- /dev/null
+++ b/scripts/sync-identical-files.py
@@ -0,0 +1,46 @@
+#!/usr/bin/env python3
+
+# Due to various technical limitations, we sometimes have files that need to be
+# kept identical in the repository. This script loads a database of such
+# files and can perform two functions: check whether they are still identical,
+# and overwrite the others with a master copy if needed.
+# The script that does the actual work is `sync-files.py`, which lives in the `codeql` submodule.
+import sys
+import os
+
+sys.path.append(os.path.realpath(os.path.join(os.path.dirname(os.path.realpath(__file__)), '../codeql/config')))
+
+import importlib
+syncfiles = importlib.import_module('sync-files')
+
+def chdir_repo_root():
+    root_path = os.path.join(os.path.dirname(os.path.abspath(__file__)), '..')
+    os.chdir(root_path)
+
+def sync_identical_files():
+    if len(sys.argv) == 1:
+        master_file_picker = lambda files: None
+    elif len(sys.argv) == 2:
+        if sys.argv[1] == "--latest":
+            master_file_picker = syncfiles.choose_latest_file
+        elif os.path.isfile(sys.argv[1]):
+            master_file_picker = lambda files: syncfiles.choose_master_file(sys.argv[1], files)
+        else:
+            raise Exception("File not found")
+    else:
+        raise Exception("Bad command line or file not found")
+    chdir_repo_root()
+    syncfiles.load_if_exists('.', 'scripts/identical-files.json')
+    for group_name, files in syncfiles.file_groups.items():
+        syncfiles.check_group(group_name, files, master_file_picker, syncfiles.emit_local_error)
+
+def main():
+    sync_identical_files()
+
+    if syncfiles.local_error_count > 0:
+        exit(1)
+    else:
+        print(__file__ +": All checks OK.")
+
+if __name__ == "__main__":
+    main()