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)