diff --git a/user_repo_source/.github/pull_request_template.md b/user_repo_source/.github/pull_request_template.md
new file mode 100644
index 00000000..b52eda11
--- /dev/null
+++ b/user_repo_source/.github/pull_request_template.md
@@ -0,0 +1,5 @@
+WARNING: 
+There is no point in opening a pull-request in this repository.
+
+This is not the relevant repository to contribute to Mathematics in Lean. This repository is cloned by people who want to study the book. It is automatically created from the source repository which can be found at  https://github.com/avigad/mathematics_in_lean_source and where you can open a pull-request.
+
diff --git a/user_repo_source/.vscode/settings.json b/user_repo_source/.vscode/settings.json
index c4c74a73..cd9f0ecf 100644
--- a/user_repo_source/.vscode/settings.json
+++ b/user_repo_source/.vscode/settings.json
@@ -19,7 +19,8 @@
         "MIL.lean": true,
         "README.md":true,
 	".lake": true,
-	".devcontainer": true
+	".devcontainer": true,
+	".github": true
     },
     "editor.minimap.enabled": false,
     "editor.acceptSuggestionOnEnter": "off",