Commit 06756a5e authored by Clément Fumex's avatar Clément Fumex
Browse files

remove absolute path to why3shell executabel, why3shell need to be in the path

parent 84dc2aa6
......@@ -27,10 +27,10 @@
proof-shell-init-cmd "fun pg_repeat f 0 = () | pg_repeat f n = (f(); pg_repeat f (n-1));"))
(defun get-prog-name ()
(concat "/home/fumex/why3/bin/why3shell " (replace-regexp-in-string ".whyitp" ".why" (buffer-file-name ()))))
(concat "why3shell " (replace-regexp-in-string ".whyitp" ".why" (buffer-file-name ()))))
(defun set-prog-name ()
(setq proof-prog-name (concat "/home/fumex/why3/bin/why3shell " (replace-regexp-in-string ".whyitp" ".why" (buffer-file-name ())))))
(setq proof-prog-name (concat "why3shell " (replace-regexp-in-string ".whyitp" ".why" (buffer-file-name ())))))
(define-derived-mode whyitp-mode proof-mode
"Why3ITP script" nil
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment