# HG changeset patch
# User haftmann
# Date 1356686139 -3600
# Node ID 264ece81df93877036668dc153c6961b99303d14
# Parent  1087c7f1d90619a5d1cf631608896b1e4d6bad86
code checking for Scala is mandatory, since Scala is now required anyway for Isabelle

diff -r 1087c7f1d906 -r 264ece81df93 src/HOL/Codegenerator_Test/Generate.thy
--- a/src/HOL/Codegenerator_Test/Generate.thy	Fri Dec 28 09:37:27 2012 +0100
+++ b/src/HOL/Codegenerator_Test/Generate.thy	Fri Dec 28 10:15:39 2012 +0100
@@ -14,6 +14,6 @@
   by a corresponding @{text export_code} command.
 *}
 
-export_code _ checking SML OCaml? Haskell? Scala?
+export_code _ checking SML OCaml? Haskell? Scala
 
 end
diff -r 1087c7f1d906 -r 264ece81df93 src/HOL/Codegenerator_Test/Generate_Pretty.thy
--- a/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Fri Dec 28 09:37:27 2012 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Fri Dec 28 10:15:39 2012 +0100
@@ -20,6 +20,6 @@
   by a corresponding @{text export_code} command.
 *}
 
-export_code _ checking SML OCaml? Haskell? Scala?
+export_code _ checking SML OCaml? Haskell? Scala
 
 end