From 2a295131a1a72dd56e6e7abdeaeca07b1b69ab6d Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel
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.
---
 printing/ppvernac.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'printing')

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index c6b1b672f8..832c08fe0e 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -627,6 +627,8 @@ module Make
           )
         | VernacTime v ->
           return (keyword "Time" ++ spc() ++ pr_vernac_list v)
+        | VernacRedirect (s, v) ->
+          return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_list v)
         | VernacTimeout(n,v) ->
           return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac v)
         | VernacFail v ->
-- 
cgit v1.2.3