From b57ca74794156f86fc0b39bc3398fb9d4befb0af Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 8 Jul 2022 23:12:11 +0200
Subject: [PATCH] chore: skip elan test if no elan found

---
 test/62/test.sh | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/test/62/test.sh b/test/62/test.sh
index 4bbad65f95..8b5a6515de 100755
--- a/test/62/test.sh
+++ b/test/62/test.sh
@@ -1,6 +1,9 @@
 #!/usr/bin/env bash
 set -euxo pipefail
 
+# skip if no elan found
+command -v elan > /dev/null || (echo "elan not found; skipping test"; exit 0)
+
 ./clean.sh
 lake +leanprover/lean4:4.0.0-m3 new foo
 cd foo