Fix scope of copyright header snippet

YaelDillies · Jan 5, 2025 · 7b5d9c7 · 7b5d9c7
1 parent 71e0190
commit 7b5d9c7
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/.vscode/copyright.code-snippets b/.vscode/copyright.code-snippets
@@ -1,6 +1,6 @@
 {
 	"Copyright header for mathlib": {
-		"scope": "lean",
+		"scope": "lean4",
 		"prefix": "copyright",
 		"body": [
 			"/-",
@@ -10,4 +10,4 @@
 			"-/"
 		]
 	}
-}
+}