From 1db34c8565729a6a2967f4e9444278a7be275b57 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 27 Sep 2017 16:05:03 +0200
Subject: Browser userscript to turn BZ#XXXX occurences into links.

---
 dev/Coq_Bugzilla_autolink.user.js | 34 ++++++++++++++++++++++++++++++++++
 1 file changed, 34 insertions(+)
 create mode 100644 dev/Coq_Bugzilla_autolink.user.js

(limited to 'dev')

diff --git a/dev/Coq_Bugzilla_autolink.user.js b/dev/Coq_Bugzilla_autolink.user.js
new file mode 100644
index 0000000000..371c5adc00
--- /dev/null
+++ b/dev/Coq_Bugzilla_autolink.user.js
@@ -0,0 +1,34 @@
+// ==UserScript==
+// @name        Coq Bugzilla autolink
+// @namespace   SkySkimmer
+// @include     https://github.com/coq/coq/*
+// @description Makes BZ#XXXX into links to bugzilla for GitHub
+// @version     1
+// @grant       none
+// ==/UserScript==
+
+var regex = /BZ#(\d+)/g;
+var substr = '<a href="https://coq.inria.fr/bugs/show_bug.cgi?id=$1">$&</a>';
+
+function doNode(node)
+{
+    node.innerHTML = node.innerHTML.replace(regex,substr);
+}
+
+var comments = document.getElementsByClassName("comment-body");
+
+for(var i=0; i<comments.length; i++)
+{
+    var pars = comments[i].getElementsByTagName("p");
+    for(var j=0; j<pars.length; j++)
+    {
+        doNode(pars[j]);
+    }
+}
+
+// usually 1 or 0 titles...
+var titles = document.getElementsByClassName("js-issue-title");
+for(var i=0; i<titles.length; i++)
+{
+    doNode(titles[i]);
+}
-- 
cgit v1.2.3