equal
deleted
inserted
replaced
35 |
35 |
36 (**********************************************************) |
36 (**********************************************************) |
37 (* Start a watcher and set up signal handlers *) |
37 (* Start a watcher and set up signal handlers *) |
38 (**********************************************************) |
38 (**********************************************************) |
39 |
39 |
40 val createWatcher : thm -> TextIO.instream * TextIO.outstream * Posix.Process.pid |
40 val createWatcher : unit -> TextIO.instream * TextIO.outstream * Posix.Process.pid |
41 |
41 |
42 |
42 |
43 |
43 |
44 (**********************************************************) |
44 (**********************************************************) |
45 (* Kill watcher process *) |
45 (* Kill watcher process *) |