diff options
Diffstat (limited to 'tools/debugger/pdb/evtchn.mli')
-rw-r--r-- | tools/debugger/pdb/evtchn.mli | 19 |
1 files changed, 0 insertions, 19 deletions
diff --git a/tools/debugger/pdb/evtchn.mli b/tools/debugger/pdb/evtchn.mli deleted file mode 100644 index 3f9560f72c..0000000000 --- a/tools/debugger/pdb/evtchn.mli +++ /dev/null @@ -1,19 +0,0 @@ -(** evtchn.mli - * - * event channel interface - * - * @author copyright (c) 2005 alex ho - * @see <www.cl.cam.ac.uk/netos/pdb> pervasive debugger - * @version 1 - *) - -val _setup : unit -> Unix.file_descr -val _bind : Unix.file_descr -> int -> unit - -val bind_interdomain : int -> int * int - - -val setup : unit -> Unix.file_descr -val read : Unix.file_descr -> int -val teardown : Unix.file_descr -> unit -val unmask : Unix.file_descr -> int -> unit |