changeset 52438 | 7b5a5116f3af |
parent 52437 | c88354589b43 |
child 52439 | 4cf3f6153eb8 |
--- a/etc/isar-keywords.el Mon Jun 24 17:03:53 2013 +0200 +++ b/etc/isar-keywords.el Mon Jun 24 17:17:17 2013 +0200 @@ -375,7 +375,6 @@ "kill" "kill_thy" "linear_undo" - "pr" "pretty_setmargin" "quit" "remove_thy" @@ -399,6 +398,7 @@ "help" "locale_deps" "nitpick" + "pr" "prf" "print_abbrevs" "print_antiquotations"