File path syntax in `doc.json`

[AndreasMatthias]

I've tested the following on a Linux system.

Some time ago file paths in doc.json were written in URI style:

file:///path/to/file.lua

Since aeb9ccb paths are written as:

//path/fo/file.lua

Note the double slash // at the beginning. I'm not certain if // is POSIX conform, but even if it were, it should be followed by a host name like //host/path/to/file.lua.

Anyway, I guess it's better to use either URI style

file:///path/to/file.lua

or a path with a single / at the beginning

/path/to/file.lua

[AndreasMatthias]

This issue is part of #2971. Closing it here.