add small fix for duplicate directory separators in relative paths (GitHub issue #15407) ok robert@ (maintainer), solene@