device-option in configure does not properly set "string with space" argument into DEV_VAL

With respect to the following lines in configure:

 device-option)
        DEV_VAR=`echo $VAL | sed "s,^\(.*\)=.*,\1,"`
        DEV_VAL=`echo $VAL | sed "s,^.*=\(.*\),\1,"`
        DeviceVar set $DEV_VAR $DEV_VAL

I think $DEV_VAL should be enclosed in quotes "" while setting via DeviceVar, so that device-option variables properly support "string with space" argument as its value.