diff options
| -rwxr-xr-x | tools/check_links.py | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tools/check_links.py b/tools/check_links.py index 14a8517c1..269e323ab 100755 --- a/tools/check_links.py +++ b/tools/check_links.py @@ -27,6 +27,8 @@ def filter_link((doc, link)): return False if link.startswith('#'): return False + if link.startswith('mailto'): + return False return True links = filter(filter_link, links) |