diff --git a/src/uws/service/file/DefaultOwnerGroupIdentifier.java b/src/uws/service/file/DefaultOwnerGroupIdentifier.java index a55645e1fed60b8098baa99c8cc26e0b8a8eef01..3087e0320acbc90c85fa649c0fe302f43f03ec77 100644 --- a/src/uws/service/file/DefaultOwnerGroupIdentifier.java +++ b/src/uws/service/file/DefaultOwnerGroupIdentifier.java @@ -44,7 +44,7 @@ public class DefaultOwnerGroupIdentifier implements OwnerGroupIdentifier { return null; else{ // The user directory name = userID in which each directory separator char are replaced by a _ (=> no confusion with a path): - String userDir = owner.getID().trim().replaceAll(File.separator, "_"); + String userDir = owner.getID().trim().replaceAll(Pattern.quote(File.separator), "_"); // The parent directory = the first LETTER of the userID or _ if none can be found: String parentDir = "_";