diff options
| -rw-r--r-- | Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -241,7 +241,7 @@ pgscripts: # Set PGHOME path in scripts back to default location. cleanpgscripts: - make pgscripts ELISP=.. + make pgscripts DEST_ELISP='$$$$HOME/ProofGeneral' ## |
