On 19-03-2017 08:01:39, Wout Mertens wrote: > * Agreed that we should make github issues available in another > format for > posterity. Perhaps just copy the text of merged PRs into /docs? (with some > tool)
I'll leave this here as a side-note: I'm working on a tool which would make this possible [0]. It is a git-based issue tracker, the proof of concept worked fine for us (a small team of two students developing this in our semesters project last semester) - currently we're re-writing it to be more stable and usable. Crawling github issues and pushing them into the repo is one of our goals. We're not there yet, but we'll get there eventually. For more information, see "doc" or open an issue, please. Don't want to hijack this thread. [0]: https://github.com/neithernut/git-dit/ -- Mit freundlichen Grüßen, Kind regards, Matthias Beyer Consider switching to free software. It adds value to your life. https://www.gnu.org/
signature.asc
Description: PGP signature
_______________________________________________ nix-dev mailing list [email protected] http://lists.science.uu.nl/mailman/listinfo/nix-dev
