From ff58b467f93a3c4bfa16ef8ea28f3c7eb2b1b007 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Thu, 19 Apr 2012 14:02:14 +0000
Subject: Fixed color refresh of command pane

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15218 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/command_windows.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'ide/command_windows.mli')

diff --git a/ide/command_windows.mli b/ide/command_windows.mli
index 8c7319aa3d..c34b6cf67a 100644
--- a/ide/command_windows.mli
+++ b/ide/command_windows.mli
@@ -11,4 +11,6 @@ class command_window :
   object
     method new_command : ?command:string -> ?term:string -> unit -> unit
     method frame : GBin.frame
+    method refresh_font : unit -> unit
+    method refresh_color : unit -> unit
   end
-- 
cgit v1.2.3