idris2 --init
doesnt check the name of a package
#6312
Loading
idris2 --init
doesnt check the name of a package
#6312