def strip_line_nums(line):
    """
    Strip line numbers from the start of a line.
    """

    # Find the end of a number at the start of the line, if there is one.
    pos = 0
    line = line.strip()
    for c in line:
        if (not c.isdigit()):
            # Don't delete numeric labels.
            if (c == ':'):
                return line
            break
        pos += 1
    return line[pos:]