Use FIXNUM_TO_DOUBLE rather than a cast. Casting a fixnum to a double

fortuitously worked under 8.0 with `native' fixnum tags but didn't
work under 7.4.

diff --git a/v7/src/microcode/fixnum.c b/v7/src/microcode/fixnum.c
index 2e8247cca3a19b4e969f36a3e1c8e4a0807be7fb..04f1d819a3c137187c32f5ef5bc402096fcf5ba1 100644 (file)
--- a/v7/src/microcode/fixnum.c
+++ b/v7/src/microcode/fixnum.c
@@ -1,6 +1,6 @@
 /* -*-C-*-
 
-$Id: fixnum.c,v 9.41 1997/07/08 03:07:06 adams Exp $
+$Id: fixnum.c,v 9.42 1997/07/15 05:09:17 adams Exp $
 
 Copyright (c) 1987-96 Massachusetts Institute of Technology
 
@@ -356,6 +356,6 @@ Equivalent to (INTEGER->FLONUM FIXNUM 2)")
 {
   PRIMITIVE_HEADER (1);
   {
-    PRIMITIVE_RETURN (double_to_flonum ((double) (arg_fixnum (1))));
+    PRIMITIVE_RETURN (double_to_flonum (FIXNUM_TO_DOUBLE (arg_fixnum (1))));
   }
 }