Constant JSVAL_TAG_MAX_DOUBLE

const JSVAL_TAG_MAX_DOUBLE: u32 = 0x1FFF0u32;