From 65fcd698bb723cc287f7ffd674fbe4ad816be974 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Manuel=20B=C3=A4renz?= <programming@manuelbaerenz.de>
Date: Thu, 15 Jul 2021 08:47:25 +0200
Subject: [PATCH] nixosTests.agda: Adapt to --guardedness requirements

The one-line test is hard to fix in a readable manner
and doesn't really add value above the hello-world test.
So rather simplify to reduce maintenance.
---
 nixos/tests/agda.nix | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/nixos/tests/agda.nix b/nixos/tests/agda.nix
index f282788519c8..ec61af2afe75 100644
--- a/nixos/tests/agda.nix
+++ b/nixos/tests/agda.nix
@@ -2,6 +2,7 @@ import ./make-test-python.nix ({ pkgs, ... }:
 
 let
   hello-world = pkgs.writeText "hello-world" ''
+    {-# OPTIONS --guardedness #-}
     open import IO
     open import Level
 
@@ -35,10 +36,6 @@ in
     machine.succeed("touch TestEmpty.agda")
     machine.succeed("agda TestEmpty.agda")
 
-    # Minimal script that actually uses the standard library
-    machine.succeed('echo "import IO" > TestIO.agda')
-    machine.succeed("agda -l standard-library -i . TestIO.agda")
-
     # Hello world
     machine.succeed(
         "cp ${hello-world} HelloWorld.agda"