From 2a295131a1a72dd56e6e7abdeaeca07b1b69ab6d Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Thu, 23 Apr 2015 01:14:49 -0400
Subject: Add a [Redirect] vernacular command

The command [Redirect "filename" (...)] redirects all the output of
[(...)]  to file "filename.out". This is useful for storing the results of
an [Eval compute], for redirecting the results of a large search, for
automatically generating traces of interesting developments, and so on.
---
 lib/pp.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'lib/pp.mli')

diff --git a/lib/pp.mli b/lib/pp.mli
index e20e5ca82..3b1123a9d 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -12,6 +12,8 @@
 val make_pp_emacs:unit -> unit
 val make_pp_nonemacs:unit -> unit
 
+val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
+
 (** Pretty-printers. *)
 
 type std_ppcmds
-- 
cgit v1.2.3