> Only one comment: if we /really/ want to be strict and pedantic, /bin/sh > uses '$' as the default prompt character, not '%' (that's csh-family). Ah! But I simply mimiced the example at the beginning of configure.html. -- Eric Botcazou