edwinb/Idris-dev — pull request #354 by yfyf (2013-06-25 22:37:09+00:00)
Title: Add bash completion file for Idris

This is far from perfect, but seems to work reasonbly well.

Also, the targets/libraries should probably not be hardcoded, but at this point
it's not clear how to dynamically generate this.

To use this add a `source $PATH_TO/idris.bash` to your `.bashrc`.

You need to have the bash-completion[1] package installed for this to work.

[1]: http://bash-completion.alioth.debian.org/