[fixup] [client] Fix package.json file due to copy/paste error.

This happened inadvertently in #588, reverting this part.
ejgallego · Oct 26, 2023 · e56b814 · e56b814
1 parent 4c836ae
commit e56b814
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/editor/code/package.json b/editor/code/package.json
@@ -157,6 +157,11 @@
         "title": "Hover",
         "type": "object",
         "properties": {
+          "coq-lsp.show_stats_on_hover": {
+            "type": "boolean",
+            "default": false,
+            "description": "Show timing and memory stats for a sentence on hover."
+          },
           "coq-lsp.show_loc_info_on_hover": {
             "type": "boolean",
             "default": false,