From 14c5ec559bcfd9fc7b1d93ff6cf04ef2e70d9209 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 26 Apr 2021 17:09:12 +0200
Subject: [PATCH] test: forgot tabs ban test

---
 tests/lean/noTabs.lean              | 4 ++++
 tests/lean/noTabs.lean.expected.out | 1 +
 2 files changed, 5 insertions(+)
 create mode 100644 tests/lean/noTabs.lean
 create mode 100644 tests/lean/noTabs.lean.expected.out

diff --git a/tests/lean/noTabs.lean b/tests/lean/noTabs.lean
new file mode 100644
index 0000000000..9475259eba
--- /dev/null
+++ b/tests/lean/noTabs.lean
@@ -0,0 +1,4 @@
+#check
+  let a := 1
+	let b := 2
+  a + b
diff --git a/tests/lean/noTabs.lean.expected.out b/tests/lean/noTabs.lean.expected.out
new file mode 100644
index 0000000000..6037902e5c
--- /dev/null
+++ b/tests/lean/noTabs.lean.expected.out
@@ -0,0 +1 @@
+noTabs.lean:3:0: error: tabs are not allowed; please configure your editor to expand them