                       (flycheck-python-verify-module 'fstar-literate "docutils"))))
   :modes '(fstar-mode fstar-literate--rst-mode))
 
-(flycheck-def-executable-var fstar-literate "python")
-
 (add-to-list 'flycheck-checkers 'fstar-literate)
 (cl-pushnew 'fstar-literate--rst-mode (flycheck-checker-get 'rst-sphinx 'modes))
 

  (let* ((prefix (concat "fslit_" (buffer-name)))
         (html-fname (make-temp-file prefix nil ".html"))
         (fst2html (expand-file-name "etc/fslit/fst2html.py" fstar--directory))
         (contents (buffer-substring-no-properties (point-min) (point-max))))
    (with-temp-buffer
      (pcase (call-process-region contents nil "python"
                                  nil t nil fst2html "-" html-fname)
        (`0 (message "Compilation complete: %s" (fstar--string-trim (buffer-string)))
            (browse-url html-fname))

(defun fstar-literate--run-converter (&rest args)
  "Run converter with ARGS on current buffer.
Return converted contents and adjusted value of point."
  (let* ((python (fstar-find-executable fstar-python-executable "Python"
                                   'fstar-python-executable 'local-only))
         (converter (expand-file-name "etc/fslit/translate.py" fstar--directory))
         (input (concat (buffer-substring-no-properties (point-min) (point))
                        fstar-literate--point-marker
