From ba560de6c33fc557a2281e2a32d289e0fc851396 Mon Sep 17 00:00:00 2001 From: Matthew-Mosior Date: Fri, 26 Jul 2024 14:20:51 -0400 Subject: [PATCH] Allowing for an empty package name. --- src/Idris/Package/Init.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Idris/Package/Init.idr b/src/Idris/Package/Init.idr index b08a2bea8..1ba1425be 100644 --- a/src/Idris/Package/Init.idr +++ b/src/Idris/Package/Init.idr @@ -112,6 +112,6 @@ interactive = do True => isIdentTrailing xs checkPackageName : List Char -> Bool - checkPackageName [] = False + checkPackageName [] = True checkPackageName (x::xs) = isIdentStart x && isIdentTrailing xs