[[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 }