aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorDavid Aspinall2009-08-28 16:56:06 +0000
committerDavid Aspinall2009-08-28 16:56:06 +0000
commit1633011392e13006aef98ccf28e67b0950021fe9 (patch)
tree1e4c4e90497f1d6626b30dbd5d87d1aa7d04388c /lib
parent37cc3165e874b5b19711753c688b076c20f76ec8 (diff)
Add convenience function for profiling
Diffstat (limited to 'lib')
-rw-r--r--lib/pg-dev.el13
1 files changed, 13 insertions, 0 deletions
diff --git a/lib/pg-dev.el b/lib/pg-dev.el
index ffcf3597..f7d66857 100644
--- a/lib/pg-dev.el
+++ b/lib/pg-dev.el
@@ -91,8 +91,21 @@
+;;;
+;;; Proling interesting packages
+;;;
+
+(defun profile-pg ()
+ (interactive)
+ (elp-instrument-package "proof-script")
+ (elp-instrument-package "proof-shell")
+ (elp-instrument-package "pg-response")
+ (elp-instrument-package "comint"))
+
+
(provide 'pg-dev)
;;; pg-dev.el ends here
+