Add a pull request template for the user repo.

The goal is to prevent PRs in the user repo.
avigad · Dec 18, 2023 · fa025d6 · fa025d6
1 parent 2298888
commit fa025d6
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 1 deletion.
diff --git a/user_repo_source/.github/pull_request_template.md 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
@@ -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",