Beside what has been stated in previous commit, actually implement
--no-ignore-file-name-case some people might be using it, it is simple enough
to implement

Note that if one plays with multiple call to both --[case-]ignore-file-name-case
the latest one wins

Convinced by: cperciva, rwatson