diff options
Diffstat (limited to '.ghcid')
| -rw-r--r-- | .ghcid | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/.ghcid b/.ghcid new file mode 100644 index 0000000000..f751a6fc83 --- /dev/null +++ b/.ghcid @@ -0,0 +1,7 @@ +--command utils/ghc-in-ghci/run.sh +--reload compiler +--reload ghc +--reload includes +--restart utils/ghc-in-ghci/run.sh +--restart utils/ghc-in-ghci/load-main.ghci +--restart utils/ghc-in-ghci/settings.ghci |