1 files changed, 9 insertions, 1 deletions
diff --git a/src/Option.cc b/src/Option.cc
index 633e9281..4c46fe92 100644
--- a/src/Option.cc
+++ b/src/Option.cc
@@ -147,12 +147,20 @@ double Option::getAsDouble(PrefPtr pref) const {
   }
 }
 
-void Option::remove(PrefPtr pref)
+void Option::removeLocal(PrefPtr pref)
 {
   unsetBit(use_, pref);
   table_[pref->i].clear();
 }
 
+void Option::remove(PrefPtr pref)
+{
+  removeLocal(pref);
+  if (parent_) {
+    parent_->remove(pref);
+  }
+}
+
 void Option::clear()
 {
   std::fill(use_.begin(), use_.end(), 0);