diff options
| author | Maxime Coste <frrrwww@gmail.com> | 2012-07-30 13:39:38 +0200 |
|---|---|---|
| committer | Maxime Coste <frrrwww@gmail.com> | 2012-07-30 13:39:38 +0200 |
| commit | a3cb9bfc5e0b26a7953ec3795944c6a6563cd7b6 (patch) | |
| tree | d14d37d9a5e96de066203980e7ede4d1cbea0f51 /src/editor.cc | |
| parent | 6bd67c01ccf8d2336400ff2fa394e4edbce73b96 (diff) | |
editor.cc: remove unused id_not_unique
Diffstat (limited to 'src/editor.cc')
| -rw-r--r-- | src/editor.cc | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/src/editor.cc b/src/editor.cc index f1b30cae..4b6ee8bc 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; |
