diff options
| author | Enrico Tassi | 2018-02-22 18:50:20 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2018-03-05 13:19:18 +0100 |
| commit | 8d2a0d56f01c907cc0a335fb19d78ee9b8c0c43d (patch) | |
| tree | e9b1f21cc0abcbfa7f1a30f275a12f5c819e13d0 /dev/doc | |
| parent | b3a8761790c0905aad8e5d3102fab606fe5e7fd6 (diff) | |
configure: make Prefs a record rather than a module of refs
In this way it is easy to support multiple defaults
Diffstat (limited to 'dev/doc')
0 files changed, 0 insertions, 0 deletions