chiark / gitweb /
Added decimal points to numbers