From 185597aef588f43fe78e9daea0b0f4ea70587da2 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 9 Dec 2019 10:16:22 +0100
Subject: [PATCH] chore: remove references to deleted lean4-server.el

---
 lean4-mode/lean4-hole.el | 2 +-
 lean4-mode/lean4-type.el | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/lean4-mode/lean4-hole.el b/lean4-mode/lean4-hole.el
index 6a31ce88cf..18457e5103 100644
--- a/lean4-mode/lean4-hole.el
+++ b/lean4-mode/lean4-hole.el
@@ -16,7 +16,7 @@
 ;; helm or company's interface would be a good addition.
 ;;
 ;;; Code:
-(require 'lean4-server)
+;(require 'lean4-server)
 
 (defun lean4-hole-handler-completing-read (alternatives)
   "Pick a hole replacement from ALTERNATIVES with `completing-read'."
diff --git a/lean4-mode/lean4-type.el b/lean4-mode/lean4-type.el
index 7215a3a679..6c57a23223 100644
--- a/lean4-mode/lean4-type.el
+++ b/lean4-mode/lean4-type.el
@@ -10,7 +10,7 @@
 (require 'dash-functional)
 (require 's)
 (require 'lean4-util)
-(require 'lean4-server)
+;(require 'lean4-server)
 (require 'lean4-debug)
 (require 'flymake)