#! /bin/sed -f
# Last edited on 1998-11-02 08:38:35 by stolfi
#
# Converts "xv" pixel data (as extracted by middle click)
# into a color in the format RRR GGG BBB / 255
#
/=/!d
s@^.*= \([0-9 ][0-9 ][0-9][, ][0-9 ][0-9 ][0-9][, ][0-9 ][0-9 ][0-9]\) *[#].*$@\1 / 255@
s/[ ][ ]\([0-9]\)[ ,]/00\1 /g
s/[ ]\([0-9][0-9]\)[ ,]/0\1 /g
s/\([0-9][0-9][0-9]\)[ ,]/\1 /g