galaxy-sixth-sensey - IdrisのREPLの設定ファイルは~/.idris/repl/init
2018/02/09
IdrisのREPLの設定ファイルは~/.idris/repl/init

“The file repl/init” と書いてあったものの、一瞬わからなかったのでメモ 🐕


この記事はこちらから修正リクエストを送ることができます。
IdrisのREPLの設定ファイルは~/.idris/repl/init - github
ゴミ箱ボタンの左にある、鉛筆ボタンを押してね!