environment: move ignore_case into repo_config_values#3

malon7782 wants to merge 2 commits into

mastermalon7782/git:masterfrom

ignore-case-0malon7782/git:ignore-case-0Copy head branch name to clipboard