From f83678f19b345425dc2f4bbbc87e70c200fb0f03 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 11 Jan 2020 13:55:31 -0800
Subject: [PATCH] chore: fix test

---
 tests/lean/run/frontend1.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index ddb0ad5bc8..11c2d75ece 100644
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@@ -61,7 +61,7 @@ pure "hello"
  #check (α : Type) → α → α
  #check {α : Type} → {β : Type} → M → (α → β) → α → β
  #check ()
- #check run
+ #check _root_.run
  end"
 
 structure S1 :=
@@ -158,7 +158,6 @@ f a
 #eval run "#check #[1, 2].foldl (fun r a => r.push a $.push a $.push a) #[]"
 #eval run "#check #[1, 2].foldl (init := #[]) $ fun r a => r.push a $.push a"
 
-
 #eval run "#check let x := one + zero; x + x"
 -- set_option trace.Elab true
 #eval run "#check (fun x => let v := x.w; v + v) s4"