return std::string(previous_filename) + ':' + std::to_string(previous_linenumber) + ':' + filename + ':' +
std::to_string(linenumber);
}
return std::string(previous_filename) + ':' + std::to_string(previous_linenumber) + ':' + filename + ':' +
std::to_string(linenumber);
}