This is supposed to end with a '/'

This commit is contained in:
Enrico Forestieri 2015-05-19 23:18:18 +02:00
parent 184a4b9d00
commit 2e78738bf0

View File

@ -1025,7 +1025,7 @@ def convert_origin(document):
if document.dir == "":
origin = "stdin"
else:
origin = document.dir.replace('\\', '/')
origin = document.dir.replace('\\', '/') + '/'
if os.name != 'nt':
origin = unicode(origin, sys.getfilesystemencoding())
document.header[i:i] = ["\\origin " + origin]