Age | Commit message (Expand) | Author |
---|---|---|
2017-11-27 | builders don't use deployment code cloned by the | Marcello Stanisci |
2017-11-27 | reverting to old style | Marcello Stanisci |
2017-11-27 | never update deployment automatically: in fact, it erases | Marcello Stanisci |
2017-01-12 | fix git updating logic | Florian Dold |
2016-06-01 | adding script to update local copy of deployment repo | Marcello Stanisci |