{"payload":{"feedbackUrl":"https://github.com/orgs/community/discussions/53140","repo":{"id":42843402,"defaultBranch":"master","name":"PG","ownerLogin":"ProofGeneral","currentUserCanPush":false,"isFork":false,"isEmpty":false,"createdAt":"2015-09-21T04:13:36.000Z","ownerAvatar":"https://avatars.githubusercontent.com/u/12037073?v=4","public":true,"private":false,"isOrgOwned":true},"refInfo":{"name":"","listCacheKey":"v0:1718799002.0","currentOid":""},"activityList":{"items":[{"before":"837f587bd5801b8b1ca30734abf3a59194959e24","after":"eca47ea8afdfcd94b4c8d88ee640f6631cfe5c5d","ref":"refs/heads/master","pushedAt":"2024-07-08T15:25:47.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"Matafou","name":"Pierre Courtieu","path":"/Matafou","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4924906?s=80&v=4"},"commit":{"message":"Merge pull request #780 from Matafou/fix-779-regression-cannot-step-Fail-correctly\n\nFixes #779 regression cannot step Fail correctly.","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2395833801\" data-permission-text=\"Title is private\" data-url=\"https://github.com/ProofGeneral/PG/issues/780\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/ProofGeneral/PG/pull/780/hovercard\" href=\"https://github.com/ProofGeneral/PG/pull/780\">#780</a> from Matafou/fix-779-regression-cannot-step-F…"}},{"before":"99f91e873ec2fdc41079555db1130f07d9a9ce89","after":"837f587bd5801b8b1ca30734abf3a59194959e24","ref":"refs/heads/master","pushedAt":"2024-07-06T17:33:34.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16718397?s=80&v=4"},"commit":{"message":"Merge pull request #777 from hendriktews/ci-update\n\nCI: update to Coq 8.19.2 and Emacs 29.4","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2377617162\" data-permission-text=\"Title is private\" data-url=\"https://github.com/ProofGeneral/PG/issues/777\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/ProofGeneral/PG/pull/777/hovercard\" href=\"https://github.com/ProofGeneral/PG/pull/777\">#777</a> from hendriktews/ci-update"}},{"before":"ffd7000505bbca3f52df36ed4a025e2bdcea07d3","after":null,"ref":"refs/heads/coq-dont-strip-cr","pushedAt":"2024-06-19T12:10:02.000Z","pushType":"branch_deletion","commitsCount":0,"pusher":{"login":"erikmd","name":"Erik Martin-Dorel","path":"/erikmd","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10367254?s=80&v=4"}},{"before":"0e0170f96f5feaeefe59052a08373080acc20393","after":"99f91e873ec2fdc41079555db1130f07d9a9ce89","ref":"refs/heads/master","pushedAt":"2024-06-19T12:09:59.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"erikmd","name":"Erik Martin-Dorel","path":"/erikmd","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10367254?s=80&v=4"},"commit":{"message":"fix(coq.el): (setq proof-shell-strip-crs-from-input nil) (#774)\n\nRelated: https://github.com/ProofGeneral/PG/issues/773","shortMessageHtmlLink":"fix(coq.el): (setq proof-shell-strip-crs-from-input nil) (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2354891473\" data-permission-text=\"Title is private\" data-url=\"https://github.com/ProofGeneral/PG/issues/774\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/ProofGeneral/PG/pull/774/hovercard\" href=\"https://github.com/ProofGeneral/PG/pull/774\">#774</a>)"}},{"before":"b9fdbbf0b50fc2c0c2ef799d05b9c6c1019d17aa","after":"0e0170f96f5feaeefe59052a08373080acc20393","ref":"refs/heads/master","pushedAt":"2024-06-19T08:41:03.000Z","pushType":"pr_merge","commitsCount":4,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16718397?s=80&v=4"},"commit":{"message":"proof-stat: admitted proofs count as failing\n\nChange `proof-check-chunks' such that Admitted proofs are reported as\nfailing.","shortMessageHtmlLink":"proof-stat: admitted proofs count as failing"}},{"before":"cb23709ad0c9a9ca0ee48b3ee73c29caea243b98","after":"b9fdbbf0b50fc2c0c2ef799d05b9c6c1019d17aa","ref":"refs/heads/master","pushedAt":"2024-06-15T15:46:55.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"Matafou","name":"Pierre Courtieu","path":"/Matafou","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/4924906?s=80&v=4"},"commit":{"message":"Merge pull request #768 from Matafou/splash-time","shortMessageHtmlLink":"Merge pull request <a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2279607100\" data-permission-text=\"Title is private\" data-url=\"https://github.com/ProofGeneral/PG/issues/768\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/ProofGeneral/PG/pull/768/hovercard\" href=\"https://github.com/ProofGeneral/PG/pull/768\">#768</a> from Matafou/splash-time"}},{"before":null,"after":"ffd7000505bbca3f52df36ed4a025e2bdcea07d3","ref":"refs/heads/coq-dont-strip-cr","pushedAt":"2024-06-15T14:28:22.000Z","pushType":"branch_creation","commitsCount":0,"pusher":{"login":"erikmd","name":"Erik Martin-Dorel","path":"/erikmd","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10367254?s=80&v=4"},"commit":{"message":"fix(coq.el): (setq proof-shell-strip-crs-from-input nil)\n\nRelated: https://github.com/ProofGeneral/PG/issues/773","shortMessageHtmlLink":"fix(coq.el): (setq proof-shell-strip-crs-from-input nil)"}},{"before":"1adcaaf4f0d09a29977d45fe5360fb1dce381803","after":"cb23709ad0c9a9ca0ee48b3ee73c29caea243b98","ref":"refs/heads/master","pushedAt":"2024-05-13T07:20:08.000Z","pushType":"pr_merge","commitsCount":4,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16718397?s=80&v=4"},"commit":{"message":"proof-stat: add test for proof-check-annotate","shortMessageHtmlLink":"proof-stat: add test for proof-check-annotate"}},{"before":"afae49509f5cf06bb8a9573444dbf0137adfd6e0","after":"1adcaaf4f0d09a29977d45fe5360fb1dce381803","ref":"refs/heads/master","pushedAt":"2024-05-02T07:46:16.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16718397?s=80&v=4"},"commit":{"message":"CI: update CI config to include Emacs 29.3","shortMessageHtmlLink":"CI: update CI config to include Emacs 29.3"}},{"before":"6cace58d0d632c4eafa18959319a484fb5c07238","after":"afae49509f5cf06bb8a9573444dbf0137adfd6e0","ref":"refs/heads/master","pushedAt":"2024-04-29T14:11:44.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16718397?s=80&v=4"},"commit":{"message":"update Coq ignored extensions and add dired-x compatibility","shortMessageHtmlLink":"update Coq ignored extensions and add dired-x compatibility"}},{"before":"1f0c75788a70fc206a060394d92736e51ccc6a9d","after":"6cace58d0d632c4eafa18959319a484fb5c07238","ref":"refs/heads/master","pushedAt":"2024-04-25T09:39:47.000Z","pushType":"pr_merge","commitsCount":9,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16718397?s=80&v=4"},"commit":{"message":"proof-stat: address review comments\n\n- read-only and no undo in report buffer\n- add a batch mode test for proof-check-proofs; require seq library to\n  make this work in Emacs 26","shortMessageHtmlLink":"proof-stat: address review comments"}},{"before":"7a28fa207a5992224c32abc988f936596f13a6b2","after":"1f0c75788a70fc206a060394d92736e51ccc6a9d","ref":"refs/heads/master","pushedAt":"2024-04-25T07:57:01.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16718397?s=80&v=4"},"commit":{"message":"ignore 3-pane mode if frame is too small\n\nFixes #760.","shortMessageHtmlLink":"ignore 3-pane mode if frame is too small"}},{"before":"d30569d8c56629cfa93fcd46e59cb52e863fe77a","after":"7a28fa207a5992224c32abc988f936596f13a6b2","ref":"refs/heads/master","pushedAt":"2024-04-20T12:54:54.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16718397?s=80&v=4"},"commit":{"message":"proof-shell, pg-response: indentation fixes","shortMessageHtmlLink":"proof-shell, pg-response: indentation fixes"}},{"before":"1a37480857b6408b0c57e655ceb302ce8f884833","after":"d30569d8c56629cfa93fcd46e59cb52e863fe77a","ref":"refs/heads/master","pushedAt":"2024-04-18T09:06:09.000Z","pushType":"pr_merge","commitsCount":3,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16718397?s=80&v=4"},"commit":{"message":"CI: extend goals present tests with Search and Check commdands\n\n- After Search and Check the goals should be up-to-date and the\n  response should be visible, also in two-pane mode.\n- Extend existing tests to check that the response is also visible in\n  two-pane mode, if applicable.\n- Use Proof General variables containing the buffer instead of buffer\n  names.","shortMessageHtmlLink":"CI: extend goals present tests with Search and Check commdands"}},{"before":"1566fd882e1618d0843cb5930632fe00b681167f","after":"1a37480857b6408b0c57e655ceb302ce8f884833","ref":"refs/heads/master","pushedAt":"2024-04-06T17:07:01.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16718397?s=80&v=4"},"commit":{"message":"coq: clear goals buffer after admitted\n\nOnly add the declaration info message to the right regular expression\nand generic Proof General will clear the goals buffer. As a side\neffect the declaration info message won't show up in the response\nbuffer any more. Need to change the tests that rely on this.","shortMessageHtmlLink":"coq: clear goals buffer after admitted"}},{"before":"2637216deea35e4a91b14c7d61a20328fe6dad84","after":"1566fd882e1618d0843cb5930632fe00b681167f","ref":"refs/heads/master","pushedAt":"2024-03-31T19:08:44.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16718397?s=80&v=4"},"commit":{"message":"CI: fix workflow problem in cipg and sync currently used containers","shortMessageHtmlLink":"CI: fix workflow problem in cipg and sync currently used containers"}},{"before":"01aa3173419ea9349ae00d3bd2b14264dd6d6c47","after":"2637216deea35e4a91b14c7d61a20328fe6dad84","ref":"refs/heads/master","pushedAt":"2024-03-28T23:44:01.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16718397?s=80&v=4"},"commit":{"message":"Revert \"texi-docstring-magic.el: Fix regression in last change\"\n\nThis reverts commit f620526756c6f24ddf40c515c6cc9bba969a6535 which was\npushed directly without running CI.","shortMessageHtmlLink":"Revert \"texi-docstring-magic.el: Fix regression in last change\""}},{"before":"f620526756c6f24ddf40c515c6cc9bba969a6535","after":"01aa3173419ea9349ae00d3bd2b14264dd6d6c47","ref":"refs/heads/master","pushedAt":"2024-03-28T22:58:18.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16718397?s=80&v=4"},"commit":{"message":"Revert \"(texi-docstring-magic-texi-for): Use `help-function-arglist`\"\n\nThis reverts commit a63a9b13185b0a2f13eb417165708f9cf38cc827 because\nit breaks CI.","shortMessageHtmlLink":"Revert \"(texi-docstring-magic-texi-for): Use <code>help-function-arglist</code>\""}},{"before":"a63a9b13185b0a2f13eb417165708f9cf38cc827","after":"f620526756c6f24ddf40c515c6cc9bba969a6535","ref":"refs/heads/master","pushedAt":"2024-03-28T22:57:09.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"monnier","name":null,"path":"/monnier","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3629383?s=80&v=4"},"commit":{"message":"texi-docstring-magic.el: Fix regression in last change\n\n* doc/PG-adapting.texi: Re-build.\n\n* lib/texi-docstring-magic.el (texi-docstring-magic-splice-sep):\nDelete function.\n(texi-docstring-magic-texi): Use `mapconcat` instead.\n(texi-docstring-magic-texi-for): Don't use obsolete `face-doc-string`.\nFollow aliasing indirections and autoload the function if needed to\nget its argument list.","shortMessageHtmlLink":"texi-docstring-magic.el: Fix regression in last change"}},{"before":"5d6cbdfe90e8e9cade6bb5184b0ded0db7666a93","after":"a63a9b13185b0a2f13eb417165708f9cf38cc827","ref":"refs/heads/master","pushedAt":"2024-03-27T18:55:18.000Z","pushType":"push","commitsCount":1,"pusher":{"login":"monnier","name":null,"path":"/monnier","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/3629383?s=80&v=4"},"commit":{"message":"(texi-docstring-magic-texi-for): Use `help-function-arglist`","shortMessageHtmlLink":"(texi-docstring-magic-texi-for): Use <code>help-function-arglist</code>"}},{"before":"01ea35f17731087541edb4d5a9b473420acd31e6","after":"5d6cbdfe90e8e9cade6bb5184b0ded0db7666a93","ref":"refs/heads/master","pushedAt":"2024-03-23T21:03:03.000Z","pushType":"pr_merge","commitsCount":2,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16718397?s=80&v=4"},"commit":{"message":"CI: store containers currently needed and adapt cipg -delete","shortMessageHtmlLink":"CI: store containers currently needed and adapt cipg -delete"}},{"before":"728bd2535c181793307c5ed7ec9fbd9cbec73d54","after":"01ea35f17731087541edb4d5a9b473420acd31e6","ref":"refs/heads/master","pushedAt":"2024-03-23T20:59:00.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16718397?s=80&v=4"},"commit":{"message":"ci: fix goals present tests (commit a6bd8185)\n\nThese tests did not run until now.","shortMessageHtmlLink":"ci: fix goals present tests (commit <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/ProofGeneral/PG/commit/a6bd8185e0af4e0a0e9f11bdffa1ffbc072a4507/hovercard\" href=\"https://github.com/ProofGeneral/PG/commit/a6bd8185e0af4e0a0e9f11bdffa1ffbc072a4507\"><tt>a6bd818</tt></a>)"}},{"before":"e793ac46a18873fab3a1d6ee80c6a5b38d25561f","after":"728bd2535c181793307c5ed7ec9fbd9cbec73d54","ref":"refs/heads/master","pushedAt":"2024-03-15T20:13:17.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16718397?s=80&v=4"},"commit":{"message":"CI: do not artificially restrict parallel test execution\n\nFor whatever reason, the test job always runs late in a CI run (I am\nblaming the max-parallel annotation for this). This leads to longer CI\nruns, because, at the end, for several rounds on 6 instances of the\ntest job are executing. Note that Github starts at most 20 of our\ntests in parallel, so it is not our responsibility to ensure that\nlimit.","shortMessageHtmlLink":"CI: do not artificially restrict parallel test execution"}},{"before":"a6f8243ed2860cc7c9cb051496f1543d981e9f7e","after":"e793ac46a18873fab3a1d6ee80c6a5b38d25561f","ref":"refs/heads/master","pushedAt":"2024-03-08T09:49:52.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16718397?s=80&v=4"},"commit":{"message":"CI: test 8.19.1 instead of 8.19.0\n\nAchieved by updating the docker containers.","shortMessageHtmlLink":"CI: test 8.19.1 instead of 8.19.0"}},{"before":"caa100e2d95bc81af6edc74bc969e1d4e13b7ca3","after":"a6f8243ed2860cc7c9cb051496f1543d981e9f7e","ref":"refs/heads/master","pushedAt":"2024-03-06T20:02:54.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16718397?s=80&v=4"},"commit":{"message":"CHANGES: add entry for 9b38f844df79eaf77a64c82d21cfdc70351ccc03","shortMessageHtmlLink":"CHANGES: add entry for <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/ProofGeneral/PG/commit/9b38f844df79eaf77a64c82d21cfdc70351ccc03/hovercard\" href=\"https://github.com/ProofGeneral/PG/commit/9b38f844df79eaf77a64c82d21cfdc70351ccc03\"><tt>9b38f84</tt></a>"}},{"before":"1f0724813a4eacb59b7a8d8905619c893d12f03b","after":"caa100e2d95bc81af6edc74bc969e1d4e13b7ca3","ref":"refs/heads/master","pushedAt":"2024-03-05T00:03:37.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"erikmd","name":"Erik Martin-Dorel","path":"/erikmd","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/10367254?s=80&v=4"},"commit":{"message":"coq-tests: fix error introduced by Cyril Anaclet in 0ae25c5a (#743)\n\nThe purpose of unwind-protect is to execute the cleanup-forms in case\r\nof a non-local exit. It does not make any sense to move these forms\r\nbehind unwind-protect.","shortMessageHtmlLink":"coq-tests: fix error introduced by Cyril Anaclet in <a class=\"commit-link\" data-hovercard-type=\"commit\" data-hovercard-url=\"https://github.com/ProofGeneral/PG/commit/0ae25c5ae3f401ad9cabe16b1636ff2e11da874c/hovercard\" href=\"https://github.com/ProofGeneral/PG/commit/0ae25c5ae3f401ad9cabe16b1636ff2e11da874c\"><tt>0ae25c5</tt></a> (<a class=\"issue-link js-issue-link\" data-error-text=\"Failed to load title\" data-id=\"2165548005\" data-permission-text=\"Title is private\" data-url=\"https://github.com/ProofGeneral/PG/issues/743\" data-hovercard-type=\"pull_request\" data-hovercard-url=\"/ProofGeneral/PG/pull/743/hovercard\" href=\"https://github.com/ProofGeneral/PG/pull/743\">#743</a>)"}},{"before":"4814efb3668ec6c6a747c6b95691ca79d9f94bca","after":"1f0724813a4eacb59b7a8d8905619c893d12f03b","ref":"refs/heads/master","pushedAt":"2024-02-23T14:05:34.000Z","pushType":"pr_merge","commitsCount":11,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16718397?s=80&v=4"},"commit":{"message":"proof-tree: protect against internal errors\n\nproof-second-action-list-active cannot be used by two packages (i.e.,\nproof-tree and coq-par-compile) simultaneously. Therefore assert it is\noff when starting a proof-tree display. Also re-initialize\nproof-tree--delayed-actions, although it should always be reset at the\nend of a proof-tree display, if everything works as expected.","shortMessageHtmlLink":"proof-tree: protect against internal errors"}},{"before":"a6bd8185e0af4e0a0e9f11bdffa1ffbc072a4507","after":"4814efb3668ec6c6a747c6b95691ca79d9f94bca","ref":"refs/heads/master","pushedAt":"2024-02-19T13:47:45.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16718397?s=80&v=4"},"commit":{"message":"proof-shell: document call graph","shortMessageHtmlLink":"proof-shell: document call graph"}},{"before":"9b38f844df79eaf77a64c82d21cfdc70351ccc03","after":"a6bd8185e0af4e0a0e9f11bdffa1ffbc072a4507","ref":"refs/heads/master","pushedAt":"2024-02-18T09:46:43.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16718397?s=80&v=4"},"commit":{"message":"add tests for checking that goals are correctly shown\n\nMost of these tests currently fail because of different instances\nof #568, see also #429, #467, #103.","shortMessageHtmlLink":"add tests for checking that goals are correctly shown"}},{"before":"4e6e5d94a7891d4fefe77652a752ba650ed78206","after":"9b38f844df79eaf77a64c82d21cfdc70351ccc03","ref":"refs/heads/master","pushedAt":"2024-02-18T09:46:02.000Z","pushType":"pr_merge","commitsCount":1,"pusher":{"login":"hendriktews","name":null,"path":"/hendriktews","primaryAvatarUrl":"https://avatars.githubusercontent.com/u/16718397?s=80&v=4"},"commit":{"message":"coq-par-compile: add user options for extra coqc/coqdep arguments\n\nUser options coq-compile-extra-coqc-arguments and\ncoq-compile-extra-coqdep-arguments are added as list of arguments to\ninvocation of, respetively, coqc and coqdep in addition to the\narguments computed, e.g., from _CoqProject.\n\nThis can be used to work around #724.","shortMessageHtmlLink":"coq-par-compile: add user options for extra coqc/coqdep arguments"}}],"hasNextPage":true,"hasPreviousPage":false,"activityType":"all","actor":null,"timePeriod":"all","sort":"DESC","perPage":30,"cursor":"djE6ks8AAAAEecGcSAA","startCursor":null,"endCursor":null}},"title":"Activity · ProofGeneral/PG"}