From 7a9df17e8520fe1b7dc6a236ef320469a8964c9f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 14 Dec 2019 14:13:21 +0100
Subject: Being explicit on existence of a remote link.

---
 theories/Logic/Hurkens.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index 9aed952183..d9e89d6b91 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -72,7 +72,7 @@
 
     - [[Geuvers01]] H. Geuvers, "Inconsistency of Classical Logic in Type
       Theory", 2001, revised 2007
-      (see {{http://www.cs.ru.nl/~herman/PUBS/newnote.ps.gz}}).
+      (see external link {{http://www.cs.ru.nl/~herman/PUBS/newnote.ps.gz}}).
 *)
 
 
-- 
cgit v1.2.3