[[project @ 2005-01-11 16:06:56 by simonmar]
simonmar**20050111160658
Rename OPTIONS to OPTIONS_GHC.
] {
hunk ./ghc/docs/users_guide/glasgow_exts.xml 4376
-
OPTIONS pragma
- OPTIONS
+ OPTIONS_GHC pragma
+ OPTIONS_GHC
hunk ./ghc/docs/users_guide/glasgow_exts.xml 4379
- pragmaOPTIONS
+ pragmaOPTIONS_GHC
hunk ./ghc/docs/users_guide/glasgow_exts.xml 4382
- The OPTIONS pragma is used to specify
+ The OPTIONS_GHC pragma is used to specify
hunk ./ghc/docs/users_guide/glasgow_exts.xml 4386
+
+ Previous versions of GHC accepted OPTIONS rather
+ than OPTIONS_GHC, but that is now deprecated.
hunk ./ghc/docs/users_guide/using.xml 54
- OPTIONS pragma OPTIONS
+ OPTIONS_GHC pragma OPTIONS_GHC
hunk ./ghc/docs/users_guide/using.xml 58
-{-# OPTIONS -fglasgow-exts #-}
+{-# OPTIONS_GHC -fglasgow-exts #-}
hunk ./ghc/docs/users_guide/using.xml 63
- OPTIONS pragmas are only looked for at
+ OPTIONS_GHC pragmas are only looked for at
hunk ./ghc/docs/users_guide/using.xml 66
- OPTIONS. Multiple OPTIONS
+ OPTIONS_GHC. Multiple OPTIONS_GHC
hunk ./ghc/docs/users_guide/using.xml 71
- you try to glob etc. inside OPTIONS.
+ you try to glob etc. inside OPTIONS_GHC.
hunk ./ghc/docs/users_guide/using.xml 73
- NOTE: the contents of OPTIONS are prepended to the
+ NOTE: the contents of OPTIONS_GHC are prepended to the
hunk ./ghc/docs/users_guide/using.xml 75
- ability to override OPTIONS settings via the command
+ ability to override OPTIONS_GHC settings via the command
hunk ./ghc/docs/users_guide/using.xml 80
- OPTIONS pragma is the Right Thing. (If you
+ OPTIONS_GHC pragma is the Right Thing. (If you
hunk ./ghc/docs/users_guide/using.xml 82
- your module, the OPTIONS will get put into the generated .hc
+ your module, the OPTIONS_GHC will get put into the generated .hc
hunk ./ghc/docs/users_guide/using.xml 105
- dynamic flag may also be given in an OPTIONS
+ dynamic flag may also be given in an OPTIONS_GHC
hunk ./ghc/docs/users_guide/using.xml 357
- file only, you'll need to use an OPTIONS
+ file only, you'll need to use an OPTIONS_GHC
}