From 6514e7e3bf12b7c1feef7f7e6153236a83745de7 Mon Sep 17 00:00:00 2001 From: Scott Guest Date: Mon, 19 Aug 2024 19:40:25 -0400 Subject: [PATCH] Don't trim separators --- k-frontend/src/main/java/org/kframework/kil/UserList.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/k-frontend/src/main/java/org/kframework/kil/UserList.java b/k-frontend/src/main/java/org/kframework/kil/UserList.java index 05f22b959cd..4c42c990daa 100644 --- a/k-frontend/src/main/java/org/kframework/kil/UserList.java +++ b/k-frontend/src/main/java/org/kframework/kil/UserList.java @@ -18,13 +18,13 @@ public class UserList extends ProductionItem { public UserList(Sort sort, String separator) { this.sort = sort; - this.separator = separator.trim(); + this.separator = separator; this.listType = ZERO_OR_MORE; } public UserList(Sort sort, String separator, String listType) { this.sort = sort; - this.separator = separator.trim(); + this.separator = separator; this.listType = listType; } @@ -58,7 +58,7 @@ public String getSeparator() { } public void setSeparator(String separator) { - this.separator = separator.trim(); + this.separator = separator; } @Override