| changeset 5291 | 23651848d638 |
| parent 5215 | b0bc8cf41ffc |
| child 5292 | 5a65d870871d |
| 5289:ed6df6b1c29a | 5291:23651848d638 |
|---|---|
1626 if path.startswith(sc): |
1626 if path.startswith(sc): |
1627 path = path[len(sc):] |
1627 path = path[len(sc):] |
1628 if path.startswith('//'): |
1628 if path.startswith('//'): |
1629 path = path[2:] |
1629 path = path[2:] |
1630 return path |
1630 return path |
1631 |
|
1632 def uirepr(s): |
|
1633 # Avoid double backslash in Windows path repr() |
|
1634 return repr(s).replace('\\\\', '\\') |