lean4-dev

Stream: Emacs

[Yury G. Kudryashov]

@Sebastian Ullrich Do you remember what was the purpose of this function?

(defun lean4-diff-test-file ()
  "Use interactive ./test_input.sh on file of current buffer"
  (interactive)
  (message (shell-command-to-string (format "yes | ./test_single.sh \"%s\" \"%s\" yes"
                                            (lean4-get-executable "lean")
                                            (f-filename (buffer-file-name))))))

[Yury G. Kudryashov]

My guess is that this is no longer relevant, and I can safely delete the file.

[Sebastian Ullrich]

It's only relevant for developing in core

[Yury G. Kudryashov]

I've removed this file for now. Please tell me if you want to have it back. If yes, then it should come with a better docstring (e.g., the docstring should contain a link to the file on Github).