Fix the case of file to be ignored with to be removed
The case of 7fc73ab5f6fbe46655855079954b26dcc14576b3, which modified .gitignore and .github/workflows/main.yml. Both files need to be
rejected and restored, but since the latter file was not there before, git checkout failed and the former file could not be restored along
with it. To fix this failure, restore the ignored files one by one.
Fix the case of file to be ignored with to be removed
The case of 7fc73ab5f6fbe46655855079954b26dcc14576b3, which modified
.gitignore
and.github/workflows/main.yml
. Both files need to berejected and restored, but since the latter file was not there before,
git checkout
failed and the former file could not be restored alongwith it. To fix this failure, restore the ignored files one by one.