diff options
| author | William Carroll <wpcarro@gmail.com> | 2020-07-01T09·38+0100 |
|---|---|---|
| committer | William Carroll <wpcarro@gmail.com> | 2020-07-01T09·38+0100 |
| commit | c4fe3c92c7e18a58630edc2a5d9a334075af985f (patch) | |
| tree | a36864e895c7b97e4cdbf6b5af96f0e090dacc03 /tools | |
| parent | d820898de597aca1b84c4ba07327dc0022a95b8c (diff) | |
Create a .ghci for this directory
I would've created on at $HOME/.ghci, but I don't need that yet, and I didn't want to bother with home-manager.
Diffstat (limited to 'tools')
0 files changed, 0 insertions, 0 deletions