#include <stdio.h>
#include <rpc/rpc.h>
#include "xdrs.h"

extern XDR_element xdrfile[MAX_NUM_XDR_FILES];

#ifdef cray
     XDR_REAL64 (int *ixdrid, float *r)
#else
void xdr_real64_(int *ixdrid, float *r)
#endif

{
    XDR 	*xdrs;
    
    xdrs = xdrfile[*ixdrid].xdrs;

    if (!xdr_double(xdrs, (double *)r)) {
	fprintf (stderr, "XDR error 64-bit real read, file %s\n",
		xdrfile[*ixdrid].filename);
	exit (-1);
    }
}
