Skip to content

Commit f70c631

Browse files
authored
Merge pull request #840 from coq-community/remove-display-goals
Remove display goals from package.json
2 parents c9cdb8b + db8ff66 commit f70c631

File tree

1 file changed

+0
-6
lines changed

1 file changed

+0
-6
lines changed

client/package.json

-6
Original file line numberDiff line numberDiff line change
@@ -253,12 +253,6 @@
253253
"category": "Coq",
254254
"title": "Reset"
255255
},
256-
{
257-
"command": "extension.coq.displayGoals",
258-
"category": "Coq",
259-
"title": "Display Goals",
260-
"description": "Displays the goal view"
261-
},
262256
{
263257
"command": "extension.coq.query.search",
264258
"category": "Coq",

0 commit comments

Comments
 (0)