{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":450408150,"defaultBranch":"master","name":"lean4-mode","ownerLogin":"leanprover-community","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2022-01-21T08:16:29.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/41703605?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1709737227.0","currentOid":""},"activityList":{"items":[{"before":"60d066fb327dbd5b0dd2ec0aa21556d087822033","after":"da7b63d854d010d621e2c82a53d6ae2d94dd53b0","ref":"refs/heads/master","pushedAt":"2024-05-13T22:22:11.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"urkud","name":"Yury G. Kudryashov","path":"/urkud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/188813?s=80&v=4"},"commit":{"message":"Locate root using \"lean-toolchain\", not \"lakefile.lean\" (#64)","shortMessageHtmlLink":"Locate root using \"lean-toolchain\", not \"lakefile.lean\" (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2293464237\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/lean4-mode/issues/64\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/lean4-mode/pull/64/hovercard\" href=\"https://github.com/leanprover-community/lean4-mode/pull/64\">#64</a>)"}},{"before":"2eccb30d18255ff44ae17e77ab46182a57caa373","after":"60d066fb327dbd5b0dd2ec0aa21556d087822033","ref":"refs/heads/master","pushedAt":"2024-04-30T14:11:52.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"urkud","name":"Yury G. Kudryashov","path":"/urkud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/188813?s=80&v=4"},"commit":{"message":"mention tactic state in README (#63)\n\n* mention tactic state in README\r\n\r\n* PR suggested edits\r\n\r\n* Update README.md\r\n\r\nCo-authored-by: Richard Copley <rcopley@gmail.com>\r\n\r\n---------\r\n\r\nCo-authored-by: Richard Copley <rcopley@gmail.com>","shortMessageHtmlLink":"mention tactic state in README (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2265876714\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/lean4-mode/issues/63\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/lean4-mode/pull/63/hovercard\" href=\"https://github.com/leanprover-community/lean4-mode/pull/63\">#63</a>)"}},{"before":"ac07247cdf546daab71d5a070477b2433e7cee01","after":"2eccb30d18255ff44ae17e77ab46182a57caa373","ref":"refs/heads/master","pushedAt":"2024-04-20T05:09:16.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"urkud","name":"Yury G. Kudryashov","path":"/urkud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/188813?s=80&v=4"},"commit":{"message":"Use project top-level for lsp-mode workspace root (#48)","shortMessageHtmlLink":"Use project top-level for lsp-mode workspace root (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1845397809\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/lean4-mode/issues/48\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/lean4-mode/pull/48/hovercard\" href=\"https://github.com/leanprover-community/lean4-mode/pull/48\">#48</a>)"}},{"before":"f1f24c15134dee3754b82c9d9924866fe6bc6b9f","after":"ac07247cdf546daab71d5a070477b2433e7cee01","ref":"refs/heads/master","pushedAt":"2024-04-10T02:47:53.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"urkud","name":"Yury G. Kudryashov","path":"/urkud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/188813?s=80&v=4"},"commit":{"message":"chore: delete unused code in \"lean4-util.el\" (#60)\n\nDelete unused functions `lean4-line-offset`, `lean4-in-comment-p`,\r\n`lean4--collect-entries`, `lean4-find-files`.","shortMessageHtmlLink":"chore: delete unused code in \"lean4-util.el\" (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2164781879\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/lean4-mode/issues/60\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/lean4-mode/pull/60/hovercard\" href=\"https://github.com/leanprover-community/lean4-mode/pull/60\">#60</a>)"}},{"before":"c20a2a95d49db007a92cfa1db215bbbe74404b52","after":"f1f24c15134dee3754b82c9d9924866fe6bc6b9f","ref":"refs/heads/master","pushedAt":"2024-03-06T15:01:41.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"urkud","name":"Yury G. Kudryashov","path":"/urkud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/188813?s=80&v=4"},"commit":{"message":"Removing unnecessary dependencies (#51)\n\n* Remove dependency on f\r\n* Remove dependency on s\r\n\r\nCo-authored-by: Richard Copley <buster@buster.me.uk>","shortMessageHtmlLink":"Removing unnecessary dependencies (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1965933520\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/lean4-mode/issues/51\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/lean4-mode/pull/51/hovercard\" href=\"https://github.com/leanprover-community/lean4-mode/pull/51\">#51</a>)"}},{"before":"46efe78023d59e7ad6dcfa9bbe21c05567883392","after":null,"ref":"refs/heads/update-abbreviations","pushedAt":"2024-03-06T15:00:27.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"urkud","name":"Yury G. Kudryashov","path":"/urkud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/188813?s=80&v=4"}},{"before":"c67803eff5e11045f1303d0165dde22944f2a7a0","after":"c20a2a95d49db007a92cfa1db215bbbe74404b52","ref":"refs/heads/master","pushedAt":"2024-03-06T15:00:25.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"urkud","name":"Yury G. Kudryashov","path":"/urkud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/188813?s=80&v=4"},"commit":{"message":"Update abbreviations.json (#57)","shortMessageHtmlLink":"Update abbreviations.json (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2161310536\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/lean4-mode/issues/57\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/lean4-mode/pull/57/hovercard\" href=\"https://github.com/leanprover-community/lean4-mode/pull/57\">#57</a>)"}},{"before":null,"after":"46efe78023d59e7ad6dcfa9bbe21c05567883392","ref":"refs/heads/update-abbreviations","pushedAt":"2024-02-29T13:48:13.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"chore: update abbreviations.json","shortMessageHtmlLink":"chore: update abbreviations.json"}},{"before":"1dbdcfa64379e150685a585019616fda10eea8e5","after":null,"ref":"refs/heads/update-abbreviations","pushedAt":"2024-02-23T17:08:44.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"urkud","name":"Yury G. Kudryashov","path":"/urkud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/188813?s=80&v=4"}},{"before":"6fbc181914c721a5a3ce079f2eba80ee1b1124a5","after":"c67803eff5e11045f1303d0165dde22944f2a7a0","ref":"refs/heads/master","pushedAt":"2024-02-23T17:08:43.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"urkud","name":"Yury G. Kudryashov","path":"/urkud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/188813?s=80&v=4"},"commit":{"message":"Update abbreviations.json (#56)","shortMessageHtmlLink":"Update abbreviations.json (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2151481949\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/lean4-mode/issues/56\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/lean4-mode/pull/56/hovercard\" href=\"https://github.com/leanprover-community/lean4-mode/pull/56\">#56</a>)"}},{"before":"80487deea65d9f4870302434dbfb9aa17992a64d","after":"1dbdcfa64379e150685a585019616fda10eea8e5","ref":"refs/heads/update-abbreviations","pushedAt":"2024-02-23T17:07:41.000Z","pushType":"force_push","commitsCount":0,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"chore: update abbreviations.json","shortMessageHtmlLink":"chore: update abbreviations.json"}},{"before":"ecd200be89e159905089fa71baeec3fb05eafa4e","after":"6fbc181914c721a5a3ce079f2eba80ee1b1124a5","ref":"refs/heads/master","pushedAt":"2024-02-23T07:41:40.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"urkud","name":"Yury G. Kudryashov","path":"/urkud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/188813?s=80&v=4"},"commit":{"message":"Don't permanently change Emacs standard-output. (#46)\n\nThe macro lean4-with-info-output-to-buffer sets the Emacs global dynamic variable standard-output to the specified buffer, and doesn't set it back to its original value. This can cause other Emacs programs to go wrong subsequently. For example, \"package.el\" assumes that standard-output has its default value, so after using lean4-mode, it is impossible to update Emacs packages.\r\n\r\nThis commit limits the duration of the change of standard-output by using let instead of setq.","shortMessageHtmlLink":"Don't permanently change Emacs standard-output. (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1822819537\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/lean4-mode/issues/46\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/lean4-mode/pull/46/hovercard\" href=\"https://github.com/leanprover-community/lean4-mode/pull/46\">#46</a>)"}},{"before":"82241b9203624fec25a14dacd8884693209c22ef","after":"ecd200be89e159905089fa71baeec3fb05eafa4e","ref":"refs/heads/master","pushedAt":"2024-02-23T07:37:02.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"urkud","name":"Yury G. Kudryashov","path":"/urkud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/188813?s=80&v=4"},"commit":{"message":"Avoid clearing echo area during info-buffer redisplay (#49)\n\nWhen the mode is entered asynchronously (for fontification in\r\n\"lean4-info-buffer-redisplay\"), calling \"set-input-method\" has the\r\nside effect of clearing the echo area, disrupting eldoc.\r\nSince the info buffer is read-only, there is no need for an input\r\nmethod.","shortMessageHtmlLink":"Avoid clearing echo area during info-buffer redisplay (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1845416218\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/lean4-mode/issues/49\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/lean4-mode/pull/49/hovercard\" href=\"https://github.com/leanprover-community/lean4-mode/pull/49\">#49</a>)"}},{"before":"d1c936409ade7d93e67107243cbc0aa55cda7fd5","after":"82241b9203624fec25a14dacd8884693209c22ef","ref":"refs/heads/master","pushedAt":"2024-02-23T07:30:28.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"urkud","name":"Yury G. Kudryashov","path":"/urkud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/188813?s=80&v=4"},"commit":{"message":"Silence byte-compiler warnings (#47)\n\nCompiling lean4-mode files in Emacs 29 gives a few warnings. These can be annoying if they cause a warning buffer to pop up during async compilation. They're not important, but they're easily fixed.","shortMessageHtmlLink":"Silence byte-compiler warnings (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1845376094\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/lean4-mode/issues/47\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/lean4-mode/pull/47/hovercard\" href=\"https://github.com/leanprover-community/lean4-mode/pull/47\">#47</a>)"}},{"before":"4bfa9d3433ec2780d377b7144199457ae3700307","after":"d1c936409ade7d93e67107243cbc0aa55cda7fd5","ref":"refs/heads/master","pushedAt":"2023-07-13T22:14:43.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"urkud","name":"Yury G. Kudryashov","path":"/urkud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/188813?s=80&v=4"},"commit":{"message":"chore: update abbreviations.json (#44)","shortMessageHtmlLink":"chore: update abbreviations.json (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1803627604\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/lean4-mode/issues/44\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/lean4-mode/pull/44/hovercard\" href=\"https://github.com/leanprover-community/lean4-mode/pull/44\">#44</a>)"}},{"before":"e7c8b27b063e275bbb39727db97c4045deb31840","after":"4bfa9d3433ec2780d377b7144199457ae3700307","ref":"refs/heads/master","pushedAt":"2023-07-13T22:14:13.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"urkud","name":"Yury G. Kudryashov","path":"/urkud","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/188813?s=80&v=4"},"commit":{"message":"Merge pull request #45 from urkud/YK-docs2","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1803656906\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/lean4-mode/issues/45\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/lean4-mode/pull/45/hovercard\" href=\"https://github.com/leanprover-community/lean4-mode/pull/45\">#45</a> from urkud/YK-docs2"}},{"before":"f4b22deffdd3bcc944efc8a7079ac8439799c90c","after":"e7c8b27b063e275bbb39727db97c4045deb31840","ref":"refs/heads/master","pushedAt":"2023-07-13T15:24:52.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"chore: update docstrings (#43)\n\nFix most of docstring issues found by `melpazoid`.","shortMessageHtmlLink":"chore: update docstrings (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1803148954\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/lean4-mode/issues/43\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/lean4-mode/pull/43/hovercard\" href=\"https://github.com/leanprover-community/lean4-mode/pull/43\">#43</a>)"}},{"before":"4f0faa79e8340272cdd2fdb7ce17066f9376e3f4","after":"f4b22deffdd3bcc944efc8a7079ac8439799c90c","ref":"refs/heads/master","pushedAt":"2023-07-13T14:34:05.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"fix: handling of multi-character output strings (#41)","shortMessageHtmlLink":"fix: handling of multi-character output strings (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1802411718\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/lean4-mode/issues/41\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/lean4-mode/pull/41/hovercard\" href=\"https://github.com/leanprover-community/lean4-mode/pull/41\">#41</a>)"}},{"before":"43f5e2b6c771602786c5b8f234e91f66ccd1b808","after":"4f0faa79e8340272cdd2fdb7ce17066f9376e3f4","ref":"refs/heads/master","pushedAt":"2023-07-13T14:31:52.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"Drop no-op menu entries and settings","shortMessageHtmlLink":"Drop no-op menu entries and settings"}},{"before":"34a263936c51746c4a83756d64e1b5832d9e336b","after":"43f5e2b6c771602786c5b8f234e91f66ccd1b808","ref":"refs/heads/master","pushedAt":"2023-05-05T10:45:07.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"fix: invalid escape in doc string (#38)","shortMessageHtmlLink":"fix: invalid escape in doc string (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1687216404\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/lean4-mode/issues/38\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/lean4-mode/pull/38/hovercard\" href=\"https://github.com/leanprover-community/lean4-mode/pull/38\">#38</a>)"}},{"before":"0cb6f61eeb639e2085c29736a7a5e8db635738a9","after":"34a263936c51746c4a83756d64e1b5832d9e336b","ref":"refs/heads/master","pushedAt":"2023-04-21T07:31:33.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"chore: refine update-abbr settings","shortMessageHtmlLink":"chore: refine update-abbr settings"}},{"before":"ac6c5b068493f7aae0fea10a5caba826d8a36585","after":"0cb6f61eeb639e2085c29736a7a5e8db635738a9","ref":"refs/heads/master","pushedAt":"2023-04-21T07:28:03.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"chore: Update abbreviations.json (#37)","shortMessageHtmlLink":"chore: Update abbreviations.json (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1677997415\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/lean4-mode/issues/37\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/lean4-mode/pull/37/hovercard\" href=\"https://github.com/leanprover-community/lean4-mode/pull/37\">#37</a>)"}},{"before":null,"after":"80487deea65d9f4870302434dbfb9aa17992a64d","ref":"refs/heads/update-abbreviations","pushedAt":"2023-04-21T07:25:28.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"github-actions[bot]","name":null,"path":"/apps/github-actions","primaryAvatarUrl":"https://avatars.githubusercontent.com/in/15368?s=80&v=4"},"commit":{"message":"[create-pull-request] automated change","shortMessageHtmlLink":"[create-pull-request] automated change"}},{"before":"c7793a57c38676933e08a385e0c9b62b39fc258e","after":"ac6c5b068493f7aae0fea10a5caba826d8a36585","ref":"refs/heads/master","pushedAt":"2023-04-21T07:24:44.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"chore: add a workflow to update abbreviations.json (#33)","shortMessageHtmlLink":"chore: add a workflow to update abbreviations.json (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1627609791\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/lean4-mode/issues/33\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/lean4-mode/pull/33/hovercard\" href=\"https://github.com/leanprover-community/lean4-mode/pull/33\">#33</a>)"}},{"before":"2c6ef33f476fdf5eb5e4fa4fa023ba8b11372440","after":"c7793a57c38676933e08a385e0c9b62b39fc258e","ref":"refs/heads/master","pushedAt":"2023-04-18T21:06:01.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"Kha","name":"Sebastian Ullrich","path":"/Kha","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/109126?s=80&v=4"},"commit":{"message":"chore: fix lint warnings (#34)\n\n* Fix headers\r\n\r\n* Lint\r\n\r\n* Add SPDX license identifiers\r\n\r\n* Update defgroup to lean4\r\n\r\n* Drop leanpkg\r\n\r\n* Checkdoc\r\n\r\n* Add license headers\r\n\r\n* Fix the URLs\r\n\r\n* Remove the functions prefixed with lean-\r\n\r\nThese functions do not exist in the repository of lean-mode (for Lean 3), so\r\nthere is no need to alias them.\r\n\r\n* Simplify the version detection\r\n\r\n* Add commentaries\r\n\r\n* Fix the header","shortMessageHtmlLink":"chore: fix lint warnings (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"1627728171\" data-permission-text=\"Title is private\" data-url=\"https://github.com/leanprover-community/lean4-mode/issues/34\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/leanprover-community/lean4-mode/pull/34/hovercard\" href=\"https://github.com/leanprover-community/lean4-mode/pull/34\">#34</a>)"}}],"hasNextPage":false,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAESOAcUAA","startCursor":null,"endCursor":null}},"title":"Activity · leanprover-community/lean4-mode"}