diff --git a/tools/rdbgui4sasa/rdbgui.ml b/tools/rdbgui4sasa/rdbgui.ml index d35a77001372f016b4f85aeab3d3b06ed306ab0e..848b262679ba23d3c9fef2742ce41abe9b20b2b7 100644 --- a/tools/rdbgui4sasa/rdbgui.ml +++ b/tools/rdbgui4sasa/rdbgui.ml @@ -46,8 +46,6 @@ let gui str = Printf.fprintf oc_stdin "%s\n" str; (* sent the session choice *) (* Printf.fprintf oc_stdin "#require \"sasa\";;\n%!" ; *) (* Printf.fprintf oc_stdin "#use \"sasa-rdbg-cmds.ml\";;\n%!"; *) - Printf.fprintf oc_stdin - "if args.suts = [] && args.envs = [] then (print_string \"quit();;\n; ignore (exit 2);;\n\")\n%!"; Printf.fprintf oc_stdin "del_hook \"print_event\"; add_hook \"print_event\" (print_sasa_event false);;\n%!"; (* Printf.fprintf oc_stdin "print_sasa_event false !e;;\n"; (* print the first event *) *)