mirror of
https://github.com/leanprover/lean4.git
synced 2026-03-17 10:24:07 +00:00
chore: enable leanprover/skills plugin for Claude Code (#12609)
This PR registers the [leanprover/skills](https://github.com/leanprover/skills) plugin marketplace in `.claude/settings.json` so that Claude Code users working on lean4 are automatically prompted to install it. Also un-ignores `.claude/settings.json` in `.gitignore` — the blanket `settings.json` rule was blocking it from being tracked. 🤖 Prepared with Claude Code
This commit is contained in:
13
.claude/settings.json
Normal file
13
.claude/settings.json
Normal file
@@ -0,0 +1,13 @@
|
||||
{
|
||||
"extraKnownMarketplaces": {
|
||||
"leanprover": {
|
||||
"source": {
|
||||
"source": "github",
|
||||
"repo": "leanprover/skills"
|
||||
}
|
||||
}
|
||||
},
|
||||
"enabledPlugins": {
|
||||
"lean@leanprover": true
|
||||
}
|
||||
}
|
||||
1
.gitignore
vendored
1
.gitignore
vendored
@@ -18,6 +18,7 @@ compile_commands.json
|
||||
*.idea
|
||||
tasks.json
|
||||
settings.json
|
||||
!.claude/settings.json
|
||||
.gdb_history
|
||||
.vscode/*
|
||||
script/__pycache__
|
||||
|
||||
Reference in New Issue
Block a user