From fc579fdc83b751a44a18d2373e86ab38806e7306 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 19 Aug 2016 02:35:47 +0200
Subject: Make the user_err header an optional parameter.

Suggested by @ppedrot
---
 tools/coqdep.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index a7c32e1d65..a9f1b73765 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -526,5 +526,5 @@ let _ =
   try
     coqdep ()
   with CErrors.UserError(s,p) ->
-    let pp = if s <> "_" then Pp.(str s ++ str ": " ++ p) else p in
+    let pp = (match s with | None -> p | Some s -> Pp.(str s ++ str ": " ++ p))  in
     Feedback.msg_error pp
-- 
cgit v1.2.3