From f65bf93607f568619fd2e87573fa5f21f3daba9d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 4 Jun 2021 12:36:04 +0200
Subject: [PATCH] try to fix shell script line endings

---
 .gitattributes | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/.gitattributes b/.gitattributes
index 258cd319..e272f6d6 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -3,3 +3,5 @@
 
 # Convert to native line endings on checkout.
 *.ref text
+# Shell scripts need Linux line endings.
+*.sh eol=lf
-- 
GitLab