Eliminate obsolete option.
authorChris Hanson <org/chris-hanson/cph>
Tue, 23 Oct 2018 02:43:51 +0000 (19:43 -0700)
committerChris Hanson <org/chris-hanson/cph>
Tue, 23 Oct 2018 02:43:51 +0000 (19:43 -0700)
commit3588dc58b9354d10b9c986b03540b35d1e4a18f5
tree8ea5fc71fb6131e703ea4be21fa030c13aac8cbd
parent701df207a7bda0b8f9c61647e1799272e4d680ed
Eliminate obsolete option.
src/runtime/optiondb.scm