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.
---
 intf/vernacexpr.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 450b1af0f..d7b269a1d 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -273,6 +273,7 @@ type vernac_expr =
   (* Control *)
   | VernacLoad of verbose_flag * string
   | VernacTime of vernac_list
+  | VernacRedirect of string * vernac_list
   | VernacTimeout of int * vernac_expr
   | VernacFail of vernac_expr
   | VernacError of exn (* always fails *)
-- 
cgit v1.2.3