windowing/windowserver/group/wsini_pointershift.ini
changeset 178 89bd4cfee505
parent 160 969102054596