From 467eb67bb960c15e1335f375af29b4121ac5262b Mon Sep 17 00:00:00 2001
From: JPR
Date: Wed, 22 May 2019 21:40:57 +0200
Subject: Fixing typos - Part 2

---
 ide/protocol/xmlprotocol.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide/protocol/xmlprotocol.ml')

diff --git a/ide/protocol/xmlprotocol.ml b/ide/protocol/xmlprotocol.ml
index e18219210f..5b37ca35ed 100644
--- a/ide/protocol/xmlprotocol.ml
+++ b/ide/protocol/xmlprotocol.ml
@@ -405,7 +405,7 @@ end = struct
           | (lg, rg) :: l ->
             Printf.sprintf "%i:%a"
               (List.length lg + List.length rg) pr_focus l in
-        Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals
+        Printf.sprintf "Still focused: [%a]." pr_focus g.bg_goals
     else
       let pr_goal { goal_hyp = hyps; goal_ccl = goal } =
         "[" ^ String.concat "; " (List.map Pp.string_of_ppcmds hyps) ^ " |- " ^
-- 
cgit v1.2.3