- if (file_name.index ('/') >= 0)
- return file_name;
- file_name.substitute ('\\', '/');
- file_name.substitute ("\"", "\\\"");
- file_name.substitute ("\'", "\\\'");
+ replace_all (file_name, '\\', '/');
+ replace_all (file_name, string ("//"), "/");