<html>

<head>

<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">

</head>

<body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">

Dear all,

<div class=""><br class="">

</div>

<div class="">As we're approaching the submission of our papers traffic is getting heavy on the repository.</div>

<div class="">Can I ask you to do a </div>

<div class=""><br class="">

</div>

<div class="">git pull</div>

<div class=""><br class="">

</div>

<div class="">before doing the </div>

<div class=""><br class="">

</div>

<div class="">git commit</div>

<div class=""><br class="">

</div>

<div class="">(usually it's the other way around).</div>

<div class=""><br class="">

</div>

<div class="">This would simplify the logs of the repo: currently every time you do a git pull, the merge will be </div>

<div class="">logged on the repo. Another advantage of doing the git pull before the commit is that you will never</div>

<div class="">be asked for merge confirmation.</div>

<div class=""><br class="">

</div>

<div class="">Thanks,</div>

<div class=""><br class="">

</div>

<div class="">Mauri</div>

<div class=""><br class="">

</div>

</body>

</html>