aboutsummaryrefslogtreecommitdiffhomepage
path: root/pg-init.el
diff options
context:
space:
mode:
authorGravatar Erik Martin-Dorel <erik@martin-dorel.org>2019-01-12 21:24:35 +0100
committerGravatar Erik Martin-Dorel <erik@martin-dorel.org>2019-01-13 02:47:43 +0100
commit237529c9dc8b267175a3879cf23a77487611ca91 (patch)
tree2902eed1766d50422d25b3708637a836af7d09e5 /pg-init.el
parent58cea1b8ffb02bc546ddb56a669d4094390d4809 (diff)
Rename pg-init.el to proof-general.el
Close ProofGeneral/PG#385 and close ProofGeneral/PG#398
Diffstat (limited to 'pg-init.el')
-rw-r--r--pg-init.el69
1 files changed, 0 insertions, 69 deletions
diff --git a/pg-init.el b/pg-init.el
deleted file mode 100644
index 0634de0b..00000000
--- a/pg-init.el
+++ /dev/null
@@ -1,69 +0,0 @@
-;;; pg-init.el --- PG init file for package.el and ELPA compatibility -*- lexical-binding:t; -*-
-
-;; This file is part of Proof General.
-
-;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003-2019 Free Software Foundation, Inc.
-;; Portions © Copyright 2001-2017 Pierre Courtieu
-;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
-;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews
-;; Portions © Copyright 2015-2017 Clément Pit-Claudel
-
-;; Author: Clément Pit-Claudel <clement.pitclaudel@live.com>
-;; URL: https://proofgeneral.github.io/
-;; Package-Requires: ((emacs "24.3"))
-;; Version: 4.5-git
-
-;; This program is free software; you can redistribute it and/or modify
-;; it under the terms of the GNU General Public License as published by
-;; the Free Software Foundation, either version 3 of the License, or
-;; (at your option) any later version.
-
-;; This program is distributed in the hope that it will be useful,
-;; but WITHOUT ANY WARRANTY; without even the implied warranty of
-;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
-;; GNU General Public License for more details.
-
-;; You should have received a copy of the GNU General Public License
-;; along with this program. If not, see <http://www.gnu.org/licenses/>.
-
-;;; Commentary:
-;;
-;; Proof General's initialization code (in generic/proof-site) is relatively
-;; complex, in part because it was written before package.el existed, and in
-;; part because package.el still doesn't look for autoloads in subdirectories.
-;; This file is a thin, package.el-friendly wrapper around generic/proof-site,
-;; suitable for execution on Emacs start-up. It serves two purposes:
-;;
-;; * Setting up the load path when byte-compiling PG.
-;; * Loading a minimal PG setup on startup (not all of Proof General, of course;
-;; mostly mode hooks and autoloads).
-
-;;; Code:
-
-;;;###autoload
-(if t (require 'proof-site
- (expand-file-name "generic/proof-site"
- (file-name-directory
- (or load-file-name buffer-file-name)))))
-
-(eval-when-compile
- ;; FIXME: This is used during installation of the ELPA package:
- ;; we presume that this file will be compiled before any of the files in
- ;; sub-directories and we presume that all files are compiled within the same
- ;; session, so we here add to load-path all the subdirectories so
- ;; that files in (say) coq/ can (require 'coq-foo) and the compiler will find
- ;; the corresponding file.
- (let ((byte-compile-directories
- '("generic" "lib"
- "coq" "easycrypt" "pghaskell" "pgocaml" "pgshell" "phox"
- ;; FIXME: These dirs used to not be listed, but I needed to add
- ;; them for the compilation to succeed for me. --Stef
- "isar" "lego" "twelf" "obsolete/plastic"))
- (root (file-name-directory
- (or load-file-name byte-compile-current-file buffer-file-name))))
- (dolist (dir byte-compile-directories)
- (add-to-list 'load-path (expand-file-name dir root)))))
-
-(provide 'pg-init)
-;;; pg-init.el ends here