[Rivet] --without-root vs --disable-root

[Hendrik Hoeth]

Hi,

the output of "./configure --help" suggests that for disabling ROOT
support the option --disable-root should be used, while what actually
helps avoiding ROOT is the option "--without-root". Maybe someone with
more auto-anything knowledge than I can take care of this in
configure.ac?

Cheers,

    Hendrik

-- 
Those who give up essential liberties for temporary safety
deserve neither liberty nor safety.   -- Benjamin Franklin