From f9f1597a06b2db51b85f1c19662b86330a4772fe Mon Sep 17 00:00:00 2001
From: Bulhwi Cha <chabulhwi@semmalgil.com>
Date: Fri, 18 Oct 2024 16:09:28 +0900
Subject: [PATCH] Ignore backup files

Files ending with a tilde suffix are backups.
---
 .gitignore      |  1 +
 vid_script.txt~ | 15 ---------------
 2 files changed, 1 insertion(+), 15 deletions(-)
 delete mode 100644 vid_script.txt~

diff --git a/.gitignore b/.gitignore
index e8593bf..b182198 100644
--- a/.gitignore
+++ b/.gitignore
@@ -3,3 +3,4 @@ lake-packages/
 .lake/
 **/.DS_Store
 .i18n/**/*.mo
+*~
diff --git a/vid_script.txt~ b/vid_script.txt~
deleted file mode 100644
index 2073e53..0000000
--- a/vid_script.txt~
+++ /dev/null
@@ -1,15 +0,0 @@
-How I made the natural number game.
-
-Peter Johnstone taught me that 0 was {}, 1 was {{}}, 2 was {{},{{}}} and so on. But what about all the people who didn't go to that class?
-
-Set theory is *one way of doing mathematics*.
-
-Type theory is *another way of doing mathematics*
-
-In mathematics, when you say "let G be a group" what you mean is that G is a set, and G has elements, and the elements are all individual "atoms", and that it is impossible to split the atom.
-
-
-A theorem
-Load of old nonsense.
-
-IDeas: geometry game,