diff options
| author | David Aspinall | 2004-03-01 11:44:48 +0000 |
|---|---|---|
| committer | David Aspinall | 2004-03-01 11:44:48 +0000 |
| commit | 6f0b4f1548d0a6c0bb811e35efcc28a339ce753c (patch) | |
| tree | 61599eee7ad0fb6e18849dcd42e184a57714111b /Makefile | |
| parent | dc8a7b6bff56cda86735b023eb09c1f2dc4dd022 (diff) | |
Fix cleanpgscripts
Diffstat (limited to 'Makefile')
| -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' ## |