diff options
| author | Gaëtan Gilbert | 2020-05-21 14:47:45 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-05-21 14:47:45 +0200 |
| commit | 0aedb0c8464d7f84a6fda9ed24290a8341fe8322 (patch) | |
| tree | 21f2c1d6d2d56243b10297cc26ca8e6648060eca /test-suite | |
| parent | 7c17979b38bebbc6730cb1b3edf5fa1329f2f001 (diff) | |
| parent | fb0caf14daff2e433dfc33ca564d49b26f7e8fb4 (diff) | |
Merge PR #12358: [topfmt] Set formatter + flush fix
Reviewed-by: JasonGross
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/misc/redirect_printing.out | 2 | ||||
| -rwxr-xr-x | test-suite/misc/redirect_printing.sh | 4 | ||||
| -rw-r--r-- | test-suite/misc/redirect_printing.v | 2 |
3 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/misc/redirect_printing.out b/test-suite/misc/redirect_printing.out new file mode 100644 index 0000000000..4f45c4d4c2 --- /dev/null +++ b/test-suite/misc/redirect_printing.out @@ -0,0 +1,2 @@ +nat_ind + : forall P : nat -> Prop, P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n diff --git a/test-suite/misc/redirect_printing.sh b/test-suite/misc/redirect_printing.sh new file mode 100755 index 0000000000..7da17407f3 --- /dev/null +++ b/test-suite/misc/redirect_printing.sh @@ -0,0 +1,4 @@ +#!/usr/bin/env bash + +$coqc misc/redirect_printing.v +diff -u redirect_test.out misc/redirect_printing.out diff --git a/test-suite/misc/redirect_printing.v b/test-suite/misc/redirect_printing.v new file mode 100644 index 0000000000..2f9096bcb8 --- /dev/null +++ b/test-suite/misc/redirect_printing.v @@ -0,0 +1,2 @@ +Set Printing Width 999999. +Redirect "redirect_test" Check nat_ind. |