summaryrefslogtreecommitdiff
path: root/test-suite/success/indelim.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success/indelim.v')
-rw-r--r--test-suite/success/indelim.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/indelim.v b/test-suite/success/indelim.v
index 91b6dee2..a962c29f 100644
--- a/test-suite/success/indelim.v
+++ b/test-suite/success/indelim.v
@@ -58,4 +58,4 @@ Inductive color := Red | Black.
Inductive option (A : Type) : Type :=
| None : option A
-| Some : A -> option A. \ No newline at end of file
+| Some : A -> option A.