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". > - raw data format is relatively simple, we can re-import it into something > else if needed There's «task export» that emits json. I would use that in preference to hacking together a parser. > It's very lightweight, e.g. it doesn't support adding comments onto tasks. It does; see «task annotate». Annotations are one line each, but can have any number of them. > 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".) Cheers, Daniel _______________________________________________ Reproducible-builds mailing list Reproducible-builds@lists.alioth.debian.org http://lists.alioth.debian.org/cgi-bin/mailman/listinfo/reproducible-builds