From 1182d8e7f736e0c6f515752ee4304fb12d4348af Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Fri, 24 Feb 2017 14:46:47 +0100 Subject: [PATCH] fix(library/module): has_sorry: check examples --- src/library/module.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/library/module.cpp b/src/library/module.cpp index 59d0341071..cd2af8ff16 100644 --- a/src/library/module.cpp +++ b/src/library/module.cpp @@ -388,6 +388,8 @@ environment update_module_defs(environment const & env, declaration const & d) { static optional should_report_sorry(name const & n) { if (n.is_anonymous()) return optional(); + if (n == name{"_example"}) + return optional(n); if (!is_internal_name(n)) return optional(n); if (!n.is_string() || n.is_atomic())