From 2171c01c6101958d3d12734ad970132b78d500d7 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 22 Dec 2023 19:17:44 +0100
Subject: Start pushing files from the fstar-split test folder

---
 tests/fstar-split/.gitignore | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 tests/fstar-split/.gitignore

(limited to 'tests/fstar-split/.gitignore')

diff --git a/tests/fstar-split/.gitignore b/tests/fstar-split/.gitignore
new file mode 100644
index 00000000..28a11147
--- /dev/null
+++ b/tests/fstar-split/.gitignore
@@ -0,0 +1 @@
+*/obj
\ No newline at end of file
-- 
cgit v1.2.3