1 files changed, 32 insertions, 0 deletions
diff --git a/utils/mkUserGuidePart/Options/Misc.hs b/utils/mkUserGuidePart/Options/Misc.hs
new file mode 100644
index 0000000000..d6a4c4eaec
--- /dev/null
+++ b/utils/mkUserGuidePart/Options/Misc.hs
@@ -0,0 +1,32 @@
+module Options.Misc where
+
+import Types
+
+miscOptions :: [Flag]
+miscOptions =
+  [ flag { flagName = "-jN"
+         , flagDescription =
+           "When compiling with ``--make``, compile ⟨N⟩ modules in parallel."
+         , flagType = DynamicFlag
+         }
+  , flag { flagName = "-fno-hi-version-check"
+         , flagDescription = "Don't complain about ``.hi`` file mismatches"
+         , flagType = DynamicFlag
+         }
+  , flag { flagName = "-fhistory-size"
+         , flagDescription = "Set simplification history size"
+         , flagType = DynamicFlag
+         }
+  , flag { flagName = "-fno-ghci-history"
+         , flagDescription =
+           "Do not use the load/store the GHCi command history from/to "++
+           "``ghci_history``."
+         , flagType = DynamicFlag
+         }
+  , flag { flagName = "-fno-ghci-sandbox"
+         , flagDescription =
+           "Turn off the GHCi sandbox. Means computations are run in "++
+           "the main thread, rather than a forked thread."
+         , flagType = DynamicFlag
+         }
+  ]