From 2fe82fe6fed72a0f8c93663c2dbf807768349cb0 Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Thu, 25 Jul 2024 11:23:52 +0200
Subject: [PATCH] test: make 1697 Linux-Debug safe

---
 tests/lean/run/1697.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/tests/lean/run/1697.lean b/tests/lean/run/1697.lean
index 6e865e6f45ba..23534e45511e 100644
--- a/tests/lean/run/1697.lean
+++ b/tests/lean/run/1697.lean
@@ -27,6 +27,13 @@ info: 3
 #guard_msgs in
 #eval! #[1,2,3][2]'sorry
 
+
+/-
+
+With this test I wanted to show that `#eval!` can be used to do unsafe operations. Under
+normal circumstances this actually works with the output below, but the `Linux Debug` CI build
+catches it and complains. Maybe too bold to have this in the test suite.
+
 /--
 warning: declaration uses 'sorry'
 ---
@@ -34,3 +41,5 @@ info: 3
 -/
 #guard_msgs in
 #eval! (#[1,2,3].pop)[2]'sorry
+
+-/