changeset 6876:92cef0f29878

(gettimeofday): If system doesn't have this, define it to give a fatal error.
author Richard M. Stallman <rms@gnu.org>
date Thu, 14 Apr 1994 12:01:31 +0000
parents 1862df471cac
children 6347a8d838c8
files lib-src/profile.c
diffstat 1 files changed, 8 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- 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