1 files changed, 1 insertions, 0 deletions

diff --git a/pptok.dat b/pptok.dat
index 7680356a..88083118 100644
--- a/pptok.dat
+++ b/pptok.dat
@@ -83,6 +83,7 @@
 %macro
 %pathsearch
 %pop
+%pragma
 %push
 %rep
 %repl