From 195d83025879cc63a56a5bb17b761f6608de43c9 Mon Sep 17 00:00:00 2001
From: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Date: Tue, 2 Apr 2019 14:19:28 +0100
Subject: [PATCH] Update archimedean.lean

---
 src/algebra/archimedean.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/algebra/archimedean.lean b/src/algebra/archimedean.lean
index 59c4fca5af463..f2e4f7d592ad5 100644
--- a/src/algebra/archimedean.lean
+++ b/src/algebra/archimedean.lean
@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 
 Archimedean groups and fields.
 -/
+--hi
 import algebra.group_power algebra.field_power
 import data.rat tactic.linarith tactic.abel