diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/Bugzilla_Coq_autolink.user.js | 25 | ||||
| -rw-r--r-- | dev/ci/ci-basic-overlay.sh | 4 |
2 files changed, 27 insertions, 2 deletions
diff --git a/dev/Bugzilla_Coq_autolink.user.js b/dev/Bugzilla_Coq_autolink.user.js new file mode 100644 index 0000000000..ed056021b3 --- /dev/null +++ b/dev/Bugzilla_Coq_autolink.user.js @@ -0,0 +1,25 @@ +// ==UserScript== +// @name Bugzilla Coq autolink +// @namespace CoqScript +// @include https://coq.inria.fr/bugs/* +// @description Makes #XXXX into links to Github Coq PRs +// @version 1 +// @grant none +// ==/UserScript== + +var regex = /#(\d+)/g; +var substr = '<a href="https://github.com/coq/coq/pull/$1">$&</a>'; + +function doNode(node) +{ + node.innerHTML = node.innerHTML.replace(regex,substr); +} + +var comments = document.getElementsByClassName("bz_comment_table")[0]; +var pars = comments.getElementsByClassName("bz_comment_text"); + +for(var j=0; j<pars.length; j++) +{ + doNode(pars[j]); +} + diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 8e7265969b..43525dcd40 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -127,5 +127,5 @@ ######################################################################## # Bignums ######################################################################## -: ${bignums_CI_BRANCH:=fix-thunk-printer} -: ${bignums_CI_GITURL:=https://github.com/ppedrot/bignums.git} +: ${bignums_CI_BRANCH:=master} +: ${bignums_CI_GITURL:=https://github.com/coq/bignums.git} |