1open testutils
2
3infix ++
4fun p1 ++ p2 = OS.Path.concat(p1,p2)
5
6val _ = tprint "Checking holpathdb bindings make it into interactive sessions"
7
8val _ = Systeml.system_ps (Globals.HOLDIR ++ "bin" ++ "hol.bare" ^ " < input > /dev/null 2>&1")
9
10exception InternalDie of string
11
12val _ = let
13  val istrmr = Exn.capture TextIO.openIn "output"
14  val istrm = case istrmr of
15                  Res i => i
16                | Exn e => raise InternalDie
17                                 ("Exception: "^General.exnMessage e)
18in
19  case TextIO.inputLine istrm of
20      SOME s =>
21      if String.isSubstring "tools/Holmake/tests/holpathdb/proj2" s then
22        OK()
23      else die ("Saw:\n  "^ s)
24    | NONE => die "Nothing in \"output\""
25end handle InternalDie s => die s;
26