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')

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]);
+}
+
-- 
cgit v1.2.3