From 59da5532225422deb53dcdd24a82637d045767b5 Mon Sep 17 00:00:00 2001
From: Ashwin K <ashwin-kumar.karnad@mpsd.mpg.de>
Date: Tue, 7 Feb 2023 14:13:57 +0000
Subject: [PATCH] Start from linux-debian11 as path

---
 install-dev23a.sh | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/install-dev23a.sh b/install-dev23a.sh
index 368bbe8..7fc488a 100755
--- a/install-dev23a.sh
+++ b/install-dev23a.sh
@@ -1,5 +1,7 @@
 #!/bin/bash
 set -e
+mkdir -p linux-debian11
+cd linux-debian11
 mkdir -p dev-23a
 cd dev-23a
 # clone repo if it doesn't exist yet
-- 
GitLab