Remove [Redirect] to absolute paths

find . -name '*.v' -print0 | xargs -0 sed -i 's/^\(\s*\)\(Redirect.*\.\)$/\1(* \2 *)/g'

When on a shared machine, the first user would create /tmp/outfile and
then the build would fail for the second user because the file already
exists and is owned by somebody else.

https://github.com/coq/coq/issues/8649

tested ok on top of c4e09295f5a8e10ea1957711da0e79661177e8a6

2 files changed, 7 insertions, 7 deletions

diff --git a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v
index c991c3454..ab610531f 100644
--- a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v
+++ b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v
@@ -89,8 +89,8 @@ Module Compilers.
 
     (*
     Set Printing Coercions.
-    Redirect "/tmp/pr" Print Compilers.ident.ident.
-    Redirect "/tmp/sm" Show Match Compilers.ident.ident.
+    (* Redirect "/tmp/pr" Print Compilers.ident.ident. *)
+    (* Redirect "/tmp/sm" Show Match Compilers.ident.ident. *)
     *)
     (*
 <<<
@@ -905,8 +905,8 @@ Module Compilers.
 
     (""" + """*
     Set Printing Coercions.
-    Redirect "/tmp/pr" Print Compilers.ident.ident.
-    Redirect "/tmp/sm" Show Match Compilers.ident.ident.
+    (* Redirect "/tmp/pr" Print Compilers.ident.ident. *)
+    (* Redirect "/tmp/sm" Show Match Compilers.ident.ident. *)
     *""" + """)
 """
 
diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v
index 1b66d6206..26a833aac 100644
--- a/src/Experiments/NewPipeline/Rewriter.v
+++ b/src/Experiments/NewPipeline/Rewriter.v
@@ -2190,7 +2190,7 @@ Z.mul @@ (?x >> 128, ?y >> 128)             --> mulhh @@ (x, y)
       Local Set Printing Depth 1000000.
       Local Set Printing Width 200.
       Import RewriterPrintingNotations.
-      Redirect "/tmp/fancy_rewrite_head" Print fancy_rewrite_head.
+      (* Redirect "/tmp/fancy_rewrite_head" Print fancy_rewrite_head. *)
     End red_fancy.
 
     Section red_nbe.
@@ -2286,7 +2286,7 @@ Z.mul @@ (?x >> 128, ?y >> 128)             --> mulhh @@ (x, y)
       Local Set Printing Depth 1000000.
       Local Set Printing Width 200.
       Import RewriterPrintingNotations.
-      Redirect "/tmp/nbe_rewrite_head" Print nbe_rewrite_head.
+      (* Redirect "/tmp/nbe_rewrite_head" Print nbe_rewrite_head. *)
     End red_nbe.
 
     Section red_arith.
@@ -2383,7 +2383,7 @@ Z.mul @@ (?x >> 128, ?y >> 128)             --> mulhh @@ (x, y)
       Local Set Printing Depth 1000000.
       Local Set Printing Width 200.
       Import RewriterPrintingNotations.
-      Redirect "/tmp/arith_rewrite_head" Print arith_rewrite_head.
+      (* Redirect "/tmp/arith_rewrite_head" Print arith_rewrite_head. *)
     End red_arith.
 
     Definition RewriteNBE {t} (e : expr.Expr (ident:=ident) t) : expr.Expr (ident:=ident) t