From d2b965837262e2e12198c611b5e4042772787723 Mon Sep 17 00:00:00 2001
From: Pavel 'LEdoian' Turinsky <ledoian@matfyz.cz>
Date: Fri, 3 Mar 2023 10:10:50 +0100
Subject: [PATCH] Add a script to initialize environment

When I get a clean repo (by cloning or by git-clean(1)), I do not want
to think about the usual commands to type, so I offload them here :-)
---
 init | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100755 init

diff --git a/init b/init
new file mode 100755
index 0000000..981c352
--- /dev/null
+++ b/init
@@ -0,0 +1,7 @@
+#!/bin/sh
+
+set -exu
+
+python3 -m venv env
+. env/bin/activate
+pip install -r requirements.txt