idris-lang/Idris-dev — pull request #1556 by Helkafen (2014-09-27 12:26:45+00:00)
Title: Allow REPL to run on another port (flag --port)

Make the REPL port configurable as suggested by a TODO note, in order to run several REPLs at the same time. Default port is still 4294.
Example: idris benchmarks/pidigits/pidigits.idr --port 5000

As a sidenote, I felt a bit uneasy with the command line option list, as it doesn't tell/enforce a lot. One could specify a port twice, or give an invalid port. Maybe we should encode these options in a more typesafe way.