def extract_gif_param(proc: str):
    """
    Extracts the parameter for an animated GIF, currently just the frame
    display duration in milliseconds, from a string that ends with an
    integer, in parentheses.
    """
    a = proc.strip(")").split("(")
    assert len(a) == 2
    return int(a[1])