fix cache usage in write.

2011-07-04 14:14:38 +01:00 · 2011-07-04 14:14:38 +01:00 · 89e23bff65
commit 89e23bff65
parent 21050891ee
1 changed files with 1 additions and 0 deletions
--- 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)