__put_user(9) on Linux

The text 754cc87fa5c7, as Debian 4.0 (Etch) shipped it.

Write a simple value into user space, with less checking.

__put_user(9) on Linux now