From 9b39f65b25ff434cddda9a312eb40e9f099d298e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 1 Feb 2019 19:15:16 +0100
Subject: Fix default goal selector error message.

---
 proofs/goal_select.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/proofs/goal_select.ml b/proofs/goal_select.ml
index cef3fd3f5e..955d797227 100644
--- a/proofs/goal_select.ml
+++ b/proofs/goal_select.ml
@@ -45,7 +45,7 @@ let parse_goal_selector = function
   | "!" -> SelectAlreadyFocused
   | "all" -> SelectAll
   | i ->
-      let err_msg = "The default selector must be \"all\" or a natural number." in
+      let err_msg = "The default selector must be \"all\", \"!\" or a natural number." in
       begin try
               let i = int_of_string i in
               if i < 0 then CErrors.user_err Pp.(str err_msg);
-- 
cgit v1.2.3