+
+int getJoystickNrFromDeviceName(char *device_name)
+{
+ char c;
+ int joystick_nr = 0;
+
+ if (device_name == NULL || device_name[0] == '\0')
+ return 0;
+
+ c = device_name[strlen(device_name) - 1];
+
+ if (c >= '0' && c <= '9')
+ joystick_nr = (int)(c - '0');
+
+ if (joystick_nr < 0 || joystick_nr >= MAX_PLAYERS)
+ joystick_nr = 0;
+
+ return joystick_nr;
+}
+
+/* ----------------------------------------------------------------- */
+/* the following is only for debugging purpose and normally not used */
+/* ----------------------------------------------------------------- */
+
+#define DEBUG_NUM_TIMESTAMPS 3
+
+void debug_print_timestamp(int counter_nr, char *message)
+{
+ static long counter[DEBUG_NUM_TIMESTAMPS][2];
+
+ if (counter_nr >= DEBUG_NUM_TIMESTAMPS)
+ Error(ERR_EXIT, "debugging: increase DEBUG_NUM_TIMESTAMPS in misc.c");
+
+ counter[counter_nr][0] = Counter();
+
+ if (message)
+ printf("%s %.2f seconds\n", message,
+ (float)(counter[counter_nr][0] - counter[counter_nr][1]) / 1000);
+
+ counter[counter_nr][1] = Counter();
+}