Many thanks for the suggestions on the naming of "byte".  I'd like to
conduct a little poll to help decide the issue.  Three proposals are
on the table:

"byte": i.e., leave things as they are.

"octet": replace "byte" by "octet"
  This makes it unambiguously clear that we're dealing with values in
  the range [0, 255].

"u8": Replace "byte-vector" by "u8vector" and lone uccurrences of
  "byte" to "u8" and "bytes" to "u8-some."

Please vote on the list by following up on this message; a simple body
consisting of "byte," "octet," or "u8" will suffice.

--
Cheers =8-} Mike
Friede, Völkerverständigung und überhaupt blabla