From 52145601d33ee3fa81ed3e291f2e4db1c6c1d622 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 5 Apr 2020 15:46:47 +0200
Subject: Coqdoc: Do not consider a _ following a « " », « ' » or « ` » as
 starting emphasis.

This is to support referring to names such as _CoqProject.
---
 tools/coqdoc/cpretty.mll | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 0f25bc8e12..61253019bd 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -284,7 +284,7 @@ let identifier =
 (* This misses unicode stuff, and it adds "[" and "]".  It's only an
    approximation of idents - used for detecting whether an underscore
    is part of an identifier or meant to indicate emphasis *)
-let nonidentchar = [^ 'A'-'Z' 'a'-'z' '_' '[' ']' '\'' '0'-'9' '@' ]
+let nonidentchar = [^ 'A'-'Z' 'a'-'z' '_' '[' ']' '\'' '0'-'9' '@' '\"' '\'' '`']
 
 let printing_token = [^ ' ' '\t']*
 
-- 
cgit v1.2.3