idris-tutorial icon indicating copy to clipboard operation
idris-tutorial copied to clipboard

Published 20 hours ago • verified publisher icon idris-lang

Use "GNU+Linux" instead of "Linux"

Open ghost opened this issue 10 years ago • 3 comments

ghost avatar Jun 30 '15 02:06 ghost

I'm a big fan of the FSF and their mission, but I don't think that their argument that we should say "GNU/Linux" makes any sense, and as the proportion of the system not made by the FSF grows, it's becoming less and less the case. I'm not in favor of merging this, unless there's some other good reason.

david-christiansen avatar Jun 30 '15 06:06 david-christiansen

Regardless of perceptions of the GNU/Linux debate, this repository has been deprecated in favour of a sphinx-based documentation that is hosted in the main development repository.

All PR for the tutorial should be made there.

jfdm avatar Jun 30 '15 07:06 jfdm

Oh, I didn't even see that it was on this repo.

Perhaps we should just get rid of this one, now that it's in the main repo?

david-christiansen avatar Jun 30 '15 09:06 david-christiansen