From c9601079959950cf47fb99d0e7c0e4fa6ce96ece Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Tue, 3 Oct 2017 15:54:18 -0400 Subject: autolink to Github PRs from Bugzilla --- dev/Bugzilla_Coq_autolink.user.js | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 dev/Bugzilla_Coq_autolink.user.js (limited to 'dev/Bugzilla_Coq_autolink.user.js') diff --git a/dev/Bugzilla_Coq_autolink.user.js b/dev/Bugzilla_Coq_autolink.user.js new file mode 100644 index 000000000..ed056021b --- /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 = '$&'; + +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