use fetch/merge instead of pull as in git-mirror.sh
authorBarış Metin <Talip-Baris.Metin@sophia.inria.fr>
Thu, 1 Jul 2010 14:18:35 +0000 (16:18 +0200)
committerBarış Metin <Talip-Baris.Metin@sophia.inria.fr>
Thu, 1 Jul 2010 14:18:35 +0000 (16:18 +0200)
commitf9ec8978a061fc13dfcf9679de031b8d6e2ed24e
tree65f0adc77c0e94af0b8b197e6c60466539f8431c
parent280a06f427faf512b8a2b754d53847ebe328f430
use fetch/merge instead of pull as in git-mirror.sh
module-tools.py