Daniel Shahaf: > Ximin Luo wrote on Mon, Oct 24, 2016 at 19:54:00 +0000: >> $ git pull >> $ ./task add "Some stuff" >> $ ./task add priority:H "Some more important stuff" >> $ git push > > And suppose the push gives an error because somebody else had just > pushed something, i.e. a race condition / conflict, what does one do > then? > > I suppose the answer is "fetch, reset --hard origin/master, and replay > the last few task commands from the shell history". >
No, `git pull --rebase` plus manual merging should work for most cases. See README for one case where you have to be careful, but everything else should be obvious. > > Note that by default, tasks are renumbered whenever a task is closed. > That means the small integer identifiers are volatile. The permanent > identifier of a task is its uuid. > > (There's a way to avoid renumbering with a «gc=off» config knob, but > upstream considers that "unsupported".) > Yes I set this already and documented it in README. Thanks for the other points re annotate/export. X -- GPG: ed25519/56034877E1F87C35 GPG: rsa4096/1318EFAC5FBBDBCE https://github.com/infinity0/pubkeys.git _______________________________________________ Reproducible-builds mailing list Reproducible-builds@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/reproducible-builds