Incidentally, this means that the JSONlab submodule is no longer needed, so it is removed in the present commit. Closes: #1907