diff options
| -rw-r--r-- | byterun/extern.c | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/byterun/extern.c b/byterun/extern.c index 79b6f7092..e0436ff4a 100644 --- a/byterun/extern.c +++ b/byterun/extern.c @@ -237,7 +237,7 @@ static void extern_rec(value v) return; } /* Check if already seen */ - if (! extern_ignore_sharing) { + if (! extern_ignore_sharing && tag != Infix_tag) { if (2 * obj_counter >= extern_table_size) resize_extern_table(); h = Hash(v); while (extern_table[h].ofs >= initial_ofs) { |