Remove user.config file, rename default.config to system.config.
authorAndrey Mokhov <andrey.mokhov@gmail.com>
Sat, 18 Jul 2015 23:15:45 +0000 (00:15 +0100)
committerAndrey Mokhov <andrey.mokhov@gmail.com>
Sat, 18 Jul 2015 23:15:45 +0000 (00:15 +0100)
commita8cfbde5e0fc9df532d739815a28ac2e022eff0d
treea61a3975cae1bd5b9d010602cc4cee64b1b88daa
parent5a4a443af1fabc548894ca9d3f75702a4b08cf21
Remove user.config file, rename default.config to system.config.
.gitignore
cfg/configure.ac
cfg/system.config.in [moved from cfg/default.config.in with 100% similarity]
cfg/user.config [deleted file]
src/Config.hs
src/Oracles.hs
src/Oracles/Option.hs