From c89972b6e24f5369217e012cce287bec60aaa2e1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 20 Jan 2020 18:53:54 -0800
Subject: [PATCH] chore: test

---
 tests/lean/run/macro2.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/tests/lean/run/macro2.lean b/tests/lean/run/macro2.lean
index 519b1cd15a..d315a7a4ba 100644
--- a/tests/lean/run/macro2.lean
+++ b/tests/lean/run/macro2.lean
@@ -21,4 +21,6 @@ macro_rules
 
 #check <| ~2 |>
 
+#check <| ~~2 |>
+
 #check <| <| 3 |> |>