idris-lang/Idris-dev — pull request #685 by jfdm (2013-11-28 11:46:41+00:00)
Title: Tutorial changes.

+ Tutorial is now developed in a separate github repo.
+ Moved examples to top-level
+ Added binary of tutorial for v0.9.10