Line directives appear to always insert a space between the prefix given as a command line argument and the actual number. Mercury however requires line directives to be in format #<num> with no space in between. Perhaps support could be added for format strings like "#%d", so that it remains backwards compatible with directives lacking the %d.
Line directives appear to always insert a space between the prefix given as a command line argument and the actual number. Mercury however requires line directives to be in format
#<num>with no space in between. Perhaps support could be added for format strings like"#%d", so that it remains backwards compatible with directives lacking the%d.