*/
+#include <stddef.h>
#include <float.h>
/* The value that blank numeric fields are set to when read in;
/* Screen width. */
extern int set_viewwidth;
+/* Approximate maximum amount of memory to use for cases, in
+ bytes. */
+extern size_t set_max_workspace;
+
#endif /* !settings_h */