[devel] Made FIXED and FLOATING options consistent in the APIs they enable
and disable.  Corrected scripts/options.awk to handle both command line
options and options specified in the .dfa files.
diff --git a/scripts/options.awk b/scripts/options.awk
index 0b80cec..234074d 100755
--- a/scripts/options.awk
+++ b/scripts/options.awk
@@ -85,6 +85,36 @@
     }
 }
 
+# variable=value
+#   Sets the given variable to the given value (the syntax is fairly
+#   free form, except for deb (you are expected to understand how to
+#   set the debug variable...)
+#
+#   This happens before the check on 'pre' below skips most of the
+#   rest of the actions, so the variable settings happen during
+#   preprocessing but are recorded in the END action too.  This
+#   allows them to be set on the command line too.
+$0 ~ /^[ 	]*everything[ 	=]*off[ 	]*$/{
+    everything = "off"
+    next
+}
+$0 ~ /^[ 	]*everything[ 	=]*on[ 	]*$/{
+    everything = "on"
+    next
+}
+$0 ~ /^[ 	]*logunsupported[ 	=]*0[ 	]*$/{
+    logunsupported = 0
+    next
+}
+$0 ~ /^[ 	]*logunsupported[ 	=]*1[ 	]*$/{
+    logunsupported = 1
+    next
+}
+$1 == "deb" && $2 == "=" && NF == 3{
+    deb = $3
+    next
+}
+
 # Preprocessing - this just copies the input file with lines
 # that need preprocessing (just chunk at present) expanded
 # The bare "pre" instead of "pre != 0" crashes under Sunos awk
@@ -153,31 +183,6 @@
     next
 }
 
-# variable=value
-#   Sets the given variable to the given value (the syntax is fairly
-#   free form, except for deb (you are expected to understand how to
-#   set the debug variable...)
-$0 ~ /^[ 	]*everything[ 	=]*off[ 	]*$/{
-    everything = "off"
-    next
-}
-$0 ~ /^[ 	]*everything[ 	=]*on[ 	]*$/{
-    everything = "on"
-    next
-}
-$0 ~ /^[ 	]*logunsupported[ 	=]*0[ 	]*$/{
-    logunsupported = 0
-    next
-}
-$0 ~ /^[ 	]*logunsupported[ 	=]*1[ 	]*$/{
-    logunsupported = 1
-    next
-}
-$1 == "deb" && $2 == "=" && NF == 3{
-    deb = $3
-    next
-}
-
 # option NAME ( (requires|enables|if) NAME* | on | off | disabled )*
 #   Declares an option 'NAME' and describes its default setting (disabled)
 #   and its relationship to other options.  The option is disabled
@@ -403,12 +408,12 @@
     if (err) exit 1
 
     if (pre) {
-    	# Record the variables
-	print "deb =", deb
+    	# Record the final value of the variables
+	print "deb =", deb >out
 	if (everything != "") {
-	    print "everything =", everything
+	    print "everything =", everything >out
         }
-	print "logunsupported =", logunsupported
+	print "logunsupported =", logunsupported >out
 	exit 0
     }