From 146cefa05de591ddec0f822fbb6eece72c7deab7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 16 Nov 2016 15:16:50 -0800
Subject: [PATCH] fix(library/init/breakpoint): missing file

---
 library/init/breakpoint.lean | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 library/init/breakpoint.lean

diff --git a/library/init/breakpoint.lean b/library/init/breakpoint.lean
new file mode 100644
index 0000000000..91f73f78ba
--- /dev/null
+++ b/library/init/breakpoint.lean
@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.meta.attribute init.meta.constructor_tactic
+
+namespace debugger
+
+def attr : user_attribute :=
+{ name  := `breakpoint,
+  descr := "breakpoint for debugger" }
+
+end debugger
+
+run_command attribute.register `debugger.attr