diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2016-12-15 09:39:00 +0100 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2016-12-15 09:39:00 +0100 |
| commit | b0553954a4324efd873f7caae85f0ebc0665883c (patch) | |
| tree | a9e66d5de552d516740270928930fc6aee6ccf32 /coq/coq-compile-common.el | |
| parent | 93a0d1ca16fd30e89e312932008106bc5503386f (diff) | |
die gracefully when visiting files in nonexisting directories
Diffstat (limited to 'coq/coq-compile-common.el')
| -rw-r--r-- | coq/coq-compile-common.el | 37 |
1 files changed, 8 insertions, 29 deletions
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 92614e7a..af3e70a4 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -420,18 +420,6 @@ or not." :safe (lambda (v) (every 'stringp v)) :group 'coq-auto-compile) -(defcustom coq-compile-ignore-library-directory t - "If non-nil, ProofGeneral does not compile modules from the coq library. -Should be `t' for normal coq users. If `nil' library modules are -compiled if their sources are newer. - -This option has currently no effect, because Proof General uses -coqdep to translate qualified identifiers into library file names -and coqdep does not output dependencies in the standard library." - :type 'boolean - :safe 'booleanp - :group 'coq-auto-compile) - (defcustom coq-coqdep-error-regexp (concat "^\\*\\*\\* Warning: in file .*, library .* is required " "and has not been found") @@ -518,23 +506,14 @@ for instance, not make sense to let ProofGeneral check if the coq standard library is up-to-date. This function is always invoked on the .vo file name, regardless whether the file would be compiled with ``-quick'' or not." - (or - (and - coq-compile-ignore-library-directory - (eq (compare-strings coq-library-directory 0 nil - lib-obj-file 0 (length coq-library-directory)) - t) - (when coq--debug-auto-compilation - (message "Ignore lib file %s" lib-obj-file)) - t) - (if (some - (lambda (dir-regexp) (string-match dir-regexp lib-obj-file)) - coq-compile-ignored-directories) - (progn - (when coq--debug-auto-compilation - (message "Ignore %s" lib-obj-file)) - t) - nil))) + (if (some + (lambda (dir-regexp) (string-match dir-regexp lib-obj-file)) + coq-compile-ignored-directories) + (progn + (when coq--debug-auto-compilation + (message "Ignore %s" lib-obj-file)) + t) + nil)) ;;; convert .vo files to .v files and module names |