REPL Инициализировать файл на Windows

Question

Где я могу поместить сценарий инициализации для idris REPL в Windows?

Если я поместить команды в

C:\Users\frankr85\Application Data\idris\repl\init 

содержимое не загружается.

Любые идеи?

Answer 1

Найдено. Это - по крайней мере, для меня - здесь:

C:\Users\frankr85\AppData\Roaming\idris\repl 

Answer 2

Каталог является %appdata%/idris/repl/ и файл инициализации является init. , т. Е. %appdata%/idris/repl/init