From a3cb9bfc5e0b26a7953ec3795944c6a6563cd7b6 Mon Sep 17 00:00:00 2001
From: Maxime Coste <frrrwww@gmail.com>
Date: Mon, 30 Jul 2012 13:39:38 +0200
Subject: [PATCH] editor.cc: remove unused id_not_unique

---
 src/editor.cc | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/src/editor.cc b/src/editor.cc
index f1b30cae3..4b6ee8bcd 100644
--- a/src/editor.cc
+++ b/src/editor.cc
@@ -290,12 +290,6 @@ void Editor::check_invariant() const
     assert(not selections().empty());
 }
 
-struct id_not_unique : public runtime_error
-{
-    id_not_unique(const String& id)
-        : runtime_error("id not unique: " + id) {}
-};
-
 void Editor::begin_edition()
 {
     ++m_edition_level;