From 1de340a8a730af078a3cec2fa900623032ef5730 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 9 Dec 2020 18:05:59 +0100 Subject: [PATCH] chore: restore old `lean4-diff-test-file` behavior --- lean4-mode/lean4-dev.el | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/lean4-mode/lean4-dev.el b/lean4-mode/lean4-dev.el index ebdb462f2e..01a713cd0f 100644 --- a/lean4-mode/lean4-dev.el +++ b/lean4-mode/lean4-dev.el @@ -12,6 +12,7 @@ (defun lean4-diff-test-file () "Use interactive ./test_input.sh on file of current buffer" (interactive) - (message (shell-command-to-string (format "PATH=%s/bin:$PATH ./test_single.sh -i \"%s\"" (lean4-get-rootdir) (f-filename (buffer-file-name)))))) + ; yes: auto-agree to copying missing files + (message (shell-command-to-string (format "yes | PATH=%s/bin:$PATH ./test_single.sh -i \"%s\"" (lean4-get-rootdir) (f-filename (buffer-file-name)))))) (provide 'lean4-dev)