diff options
Diffstat (limited to 'otherlibs/labltk/browser/shell.mli')
| -rw-r--r-- | otherlibs/labltk/browser/shell.mli | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/otherlibs/labltk/browser/shell.mli b/otherlibs/labltk/browser/shell.mli deleted file mode 100644 index adea44551..000000000 --- a/otherlibs/labltk/browser/shell.mli +++ /dev/null @@ -1,20 +0,0 @@ -(* $Id$ *) - -(* toplevel shell *) - -class shell : - textw:Widget.text Widget.widget -> prog:string -> - args:string array -> env:string array -> - object - method alive : bool - method kill : unit - method interrupt : unit - method insert : string -> unit - method send : string -> unit - method history : [`next|`previous] -> unit - end - -val kill_all : unit -> unit -val get_all : unit -> (string * shell) list - -val f : prog:string -> title:string -> unit |