From 5124c3fa924ba3c63bad8fca5165363b0f587112 Mon Sep 17 00:00:00 2001
From: Andrin Bertschi <hi@abertschi.ch>
Date: Fri, 19 Apr 2024 17:50:42 +0200
Subject: [PATCH] build: add ci

---
 misc/ci.sh | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/misc/ci.sh b/misc/ci.sh
index 034f6ba..f2cd94b 100755
--- a/misc/ci.sh
+++ b/misc/ci.sh
@@ -21,7 +21,12 @@ function check_pgm() {
 
 function ssh() {
     cd $root_dir/userspace/ssh
-    make
+
+    #
+    # github runner fails
+    # /usr/bin/mkdir: cannot create directory ‘/var/empty’: Permission denied
+    # ignore
+    make || true
 }
 
 function sudo() {