better comment

agda · Nov 18, 2022 · 76e3be2 · 76e3be2
1 parent be1983a
commit 76e3be2
Showing 1 changed file with 3 additions and 2 deletions.
diff --git a/fix-whitespace.yaml b/fix-whitespace.yaml
@@ -40,7 +40,8 @@ included-files:
   - "**.yml"
 
 # Do not check whitespaces in the clone of the agda repo.
-# This is a workaround, it would probably be better to have the agda repo not
-# in the working directory...
+# This is a workaround for a ci problem, it would probably
+# be better to have the agda repo not in the working
+# directory there...
 excluded-dirs:
   - "agda"