diff -r a767e9c400fa -r 8093b9e14b75 src/eric7/SystemUtilities/FileSystemUtilities.py
--- a/src/eric7/SystemUtilities/FileSystemUtilities.py Fri Feb 23 16:48:45 2024 +0100
+++ b/src/eric7/SystemUtilities/FileSystemUtilities.py Fri Feb 23 16:49:42 2024 +0100
@@ -793,7 +793,11 @@
@return device file name
@rtype str
"""
- return f"{_DeviceFileMarker}{fileName}"
+ if fileName.startswith(_DeviceFileMarker):
+ # it is already a device file name
+ return fileName
+ else:
+ return f"{_DeviceFileMarker}{fileName}"
def isDeviceFileName(fileName):
@@ -817,7 +821,11 @@
@return remote file name
@rtype str
"""
- return f"{_RemoteFileMarker}{fileName}"
+ if fileName.startswith(_RemoteFileMarker):
+ # it is already a remote file name
+ return fileName
+ else:
+ return f"{_RemoteFileMarker}{fileName}"
def isRemoteFileName(fileName):
