option vs. make-option Anthony Carrico 29 Oct 2002 15:25 UTC

Should the option constructor be "option" as in the draft or
"make-option".

  -Tony Carrico