From a77519ba1045d23a7bb8ea1c56cc90518e9fedb9 Mon Sep 17 00:00:00 2001
From: aarne <unknown>
Date: Wed, 16 Jun 2004 14:49:50 +0000
Subject: bug fixes ; command so ; reintroduce batch mode

---
 src/GF/Infra/Option.hs | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'src/GF/Infra/Option.hs')

diff --git a/src/GF/Infra/Option.hs b/src/GF/Infra/Option.hs
index c04d40244..dcfbc3b17 100644
--- a/src/GF/Infra/Option.hs
+++ b/src/GF/Infra/Option.hs
@@ -148,6 +148,9 @@ beVerbose    = iOpt "v"
 showInfo     = iOpt "i"
 beSilent     = iOpt "s"
 emitCode     = iOpt "o"
+getHelp      = iOpt "help"
+doMake       = iOpt "make"
+doBatch      = iOpt "batch"
 notEmitCode  = iOpt "noemit"
 makeMulti    = iOpt "multi"
 beShort      = iOpt "short"
-- 
cgit v1.2.3