aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Paul Steckler <steck@stecksoft.com>2017-10-03 15:54:18 -0400
committerGravatar Paul Steckler <steck@stecksoft.com>2017-10-03 15:54:18 -0400
commitc9601079959950cf47fb99d0e7c0e4fa6ce96ece (patch)
treebe1e964069ea825a3c63e9015ad43e53bf47cc81
parent2b9a34e2ffb2bf066b3b0f8452e35622519cae1c (diff)
autolink to Github PRs from Bugzilla
-rw-r--r--dev/Bugzilla_Coq_autolink.user.js25
1 files changed, 25 insertions, 0 deletions
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 = '<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]);
+}
+