# HG changeset patch
# User Richard M. Stallman <rms@gnu.org>
# Date 766324891 0
# Node ID 92cef0f2987891263b6105f91b17464ecc15c74d
# Parent  1862df471cac7d57b62f74118fbb35bb84f41da2
(gettimeofday): If system doesn't have this, define it to give a fatal error.

diff -r 1862df471cac -r 92cef0f29878 lib-src/profile.c
--- a/lib-src/profile.c	Thu Apr 14 11:59:28 1994 +0000
+++ b/lib-src/profile.c	Thu Apr 14 12:01:31 1994 +0000
@@ -38,6 +38,14 @@
 static int watch_not_started = 1; /* flag */
 static char time_string[30];
 
+#ifndef HAVE_GETTIMEOFDAY
+gettimeofday ()
+{
+  fprintf (stderr, "profile: this system does not support gettimeofday\n");
+  exit (1);
+}
+#endif
+
 /* Reset the stopwatch to zero.  */
 
 int