| changeset 76157 | ff404465b20d |
| parent 76154 | dfddb80fc515 |
| child 76159 | 361cfb8e3648 |
| 76156:e73025785dc7 | 76157:ff404465b20d |
|---|---|
7 |
7 |
8 package isabelle |
8 package isabelle |
9 |
9 |
10 |
10 |
11 import java.util.{Map => JMap} |
11 import java.util.{Map => JMap} |
12 import java.net.ServerSocket |
|
13 |
12 |
14 |
13 |
15 object SSH { |
14 object SSH { |
16 /* target machine: user@host syntax */ |
15 /* target machine: user@host syntax */ |
17 |
16 |