aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/flags.ml17
-rw-r--r--lib/flags.mli3
2 files changed, 0 insertions, 20 deletions
diff --git a/lib/flags.ml b/lib/flags.ml
index 68e287f693..f2ab87b4b7 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -86,23 +86,6 @@ let is_unsafe s = Stringset.mem s !unsafe_set
let noglob = ref false
let dump = ref false
-let dump_file = ref ""
-let dump_into_file f = dump := true; dump_file := f
-
-let dump_buffer = Buffer.create 8192
-
-let dump_string = Buffer.add_string dump_buffer
-
-let dump_it () =
- if !dump then begin
- let mode = [Open_wronly; Open_creat] in
- let c = open_out_gen mode 0o666 !dump_file in
- output_string c (Buffer.contents dump_buffer);
- Buffer.clear dump_buffer;
- close_out c
- end
-
-let _ = at_exit dump_it
(* Flags.for the virtual machine *)
diff --git a/lib/flags.mli b/lib/flags.mli
index 08f9a279d1..4cab303815 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -61,9 +61,6 @@ val is_unsafe : string -> bool
val noglob : bool ref
val dump : bool ref
-val dump_into_file : string -> unit
-val dump_string : string -> unit
-val dump_it : unit -> unit
(* Options for the virtual machine *)