Re: ** to GIT source users ** Some incompatibility in "StyleTab"

[Christopher Roy Bratusek]

I guess it would be best to remove tabs-raise-on-hover user-option and assume 
it as hardcoded-default. Any objections?

Chris