WHAT IS THIS?
This is a throwaway script to get all extensions to Mediawiki, check them out and merge them into one gigantic repo. Don't get the purpose? Ask https://github.com/jeroendedauw
This script depends on gitpython. Get it here: https://github.com/gitpython-developers/GitPython
If you have downloaded the source code:
python setup.py install
or if you want to obtain a copy more easily:
A distribution package can be obtained for manual installation at:
RUN THE SCRIPT
It's as easy as that. It might take a second or two, though.