on master help sign in
Merge branch 'master' of github.com:idris-lang/Idris-dev
commit92789a904fa59ef50be8b1a4716185097fa0e062 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 18 Feb 2014, 15:43 (13 years ago) parenta5ee4dea73cc7a
1 file changed+1−1
main/Main.hs+1−1
main/Main.hs+1−1
@@ -127,7 +127,7 @@ usagemsg = usagemsghdr ++ "\n" ++
127127 "\t --target=TRIPLE Select target triple (for llvm codegen)\n" ++
128128 "\t -S --codegenonly Do no further compilation of code generator output\n" ++
129129 "\t -c --compileonly Compile to object files rather than an executable\n" ++
130− "\t -X --extension ITEM Undocumented\n" ++
130+ "\t -X --extension EXT Turn on langage extension (TypeProviders or ErrorReflection)\n" ++
131131 "\t --dumpdefuns Undocumented\n" ++
132132 "\t --dumpcases Undocumented\n" ++
133133 "\t --log LEVEL --loglevel Debugging log level\n" ++