the filter permissions have a bug^D^D undocumented feature

I was rather concerned.
I had PHP input format set, so that nobody could use it. But on my site I could still use them (not being UID1). I searched all my settings and my permissions. But found nothing. So I contacted the security team, because apparantly I found a sec. breach!

However, when I dove into the code, I can across the very (ahum) well documented feature:
// Administrators can always use all input formats. In a way this feature makes sense, from developers/code point of view. But I think that from users/admin site it looks really weird to find out that you have not given Joe and Jane permissions to add PHP content, yet you see them adding PHP input anyway.

Right, the deeper lying logic behind this is for later. IMO the concept of filters and permissions needs an overhaul anyway. But again: later. What I have in mind is moving the permissions to the place where they belong: access control/permissions. "use Full HTML input format" permission et al. But again: later, post 4.7.

This patch simply documents this oddity. One liner. Small change.