From 89e23bff656fd97de809fbb840b54556a7076642 Mon Sep 17 00:00:00 2001
From: Vitor Santos Costa <vsc@dcc.fc.up.pt>
Date: Mon, 4 Jul 2011 14:14:38 +0100
Subject: [PATCH] fix cache usage in write.

---
 C/write.c | 1 +
 1 file changed, 1 insertion(+)

diff --git a/C/write.c b/C/write.c
index cc8a3c15b..23f44c607 100755
--- a/C/write.c
+++ b/C/write.c
@@ -197,6 +197,7 @@ write_mpint(MP_INT *big, wrf writewch) {
 static void 
 writebig(Term t, int p, int depth, int rinfixarg, struct write_globs *wglb, struct rewind_term *rwt)
 {
+  CACHE_REGS
   CELL *pt = RepAppl(t)+1;
 #ifdef USE_GMP
   if (pt[0] == BIG_INT)