aboutsummaryrefslogtreecommitdiffhomepage
path: root/etc/isar
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2009-09-11 12:06:52 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2009-09-11 12:06:52 +0000
commit21e952d79da3f466c4f10417ffd97e8f992196a8 (patch)
tree1ad39fdd75b4a93933e0a0ded941b52e6c128846 /etc/isar
parent168bf80e85be57d22f37ec003790212119e3607b (diff)
Update temp list
Diffstat (limited to 'etc/isar')
-rw-r--r--etc/isar/profiling.txt3
1 files changed, 3 insertions, 0 deletions
diff --git a/etc/isar/profiling.txt b/etc/isar/profiling.txt
index 8a5df44e..c9c0b883 100644
--- a/etc/isar/profiling.txt
+++ b/etc/isar/profiling.txt
@@ -609,3 +609,6 @@ proof-pbp-focus-on-first-goal 1 1e-0
proof-display-and-keep-buffer 1 1e-06 1e-06
proof-release-lock 1 1e-06 1e-06
pg-finish-tracing-display 1 1e-06 1e-06
+
+
+-----------------------------------------------------------------