max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove references to deleted lean4-server.el

Browse source
This commit is contained in:
Sebastian Ullrich 2019-12-09 10:16:22 +01:00
parent c7b8a03b14
commit 185597aef5
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
lean4-mode/lean4-hole.el
View file

@ -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'."

2
lean4-mode/lean4-type.el
View file

@ -10,7 +10,7 @@
(require 'dash-functional)
(require 's)
(require 'lean4-util)
(require 'lean4-server)
;(require 'lean4-server)
(require 'lean4-debug)
(require 'flymake)