diff options
| -rw-r--r-- | lib/pg-dev.el | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/lib/pg-dev.el b/lib/pg-dev.el index 491c92ba..723e1e59 100644 --- a/lib/pg-dev.el +++ b/lib/pg-dev.el @@ -97,14 +97,12 @@ (defun profile-pg () (interactive) - (elp-instrument-package "proof-script") - (elp-instrument-package "proof-shell") - (elp-instrument-package "pg-response") - (elp-instrument-package "comint") + (elp-instrument-package "proof-") + (elp-instrument-package "pg-") (elp-instrument-package "scomint") (elp-instrument-package "unicode-tokens") (elp-instrument-package "coq") - (elp-instrument-package "isar")) + (elp-instrument-package "isar")) |