From 31b7eea8489d84ae3abdb068aaf15a6fcdb02124 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Fri, 19 Oct 2018 17:18:52 -0400
Subject: More telegraphic error text for clashing URL prefixes (closes #111)

---
 src/tag.sml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/tag.sml b/src/tag.sml
index 94e5d44f..3040c36c 100644
--- a/src/tag.sml
+++ b/src/tag.sml
@@ -124,7 +124,7 @@ fun exp uf env (e, s) =
                                              ()
                                          else
                                              ErrorMsg.errorAt loc 
-                                                              ("Duplicate HTTP tag "
+                                                              ("Duplicate URL prefix "
                                                                ^ s);
                                          if ek = ek' then
                                              ()
-- 
cgit v1.2.3