From c31ba658bff3e5bb5789b4370d1267ce172c8966 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Fri, 28 Oct 2016 23:02:25 +0200
Subject: [PATCH] optionmap: remove superfluous code

This was noticed while looking at a false-positive in the report for
PVS-Studio, in #192.

* spot/misc/optionmap.cc: Do not remove the option from unused_ twice..
---
 spot/misc/optionmap.cc | 1 -
 1 file changed, 1 deletion(-)

diff --git a/spot/misc/optionmap.cc b/spot/misc/optionmap.cc
index c092f0fc0..68cee3662 100644
--- a/spot/misc/optionmap.cc
+++ b/spot/misc/optionmap.cc
@@ -182,7 +182,6 @@ namespace spot
   int
   option_map::operator[](const char* option) const
   {
-    unused_.erase(option);
     return get(option);
   }