<!-- These are just some suggestions for things you might want to include. Feel free to remove any parts that aren't relevant to you. --> ### Describe the solution you'd like <!-- Provide a clear and concise description of what you want to happen. --> Simplest solution; forward to the github project. ### What problem would this solve? <!-- In case you think it isn't obvious. If it's obvious, feel free to remove this part. We'll ask if it's not obvious to us. --> Get rid of a redundant outdated git repo. ### Describe alternatives you've considered <!-- Let us know about other solutions you've tried or researched, if any. --> mirror github repo or simply delete