code checking for Scala is mandatory, since Scala is now required anyway for Isabelle
authorhaftmann
Fri, 28 Dec 2012 10:15:39 +0100
changeset 50629 264ece81df93
parent 50628 1087c7f1d906
child 50630 1ea90e8046dc
code checking for Scala is mandatory, since Scala is now required anyway for Isabelle
src/HOL/Codegenerator_Test/Generate.thy
src/HOL/Codegenerator_Test/Generate_Pretty.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
--- 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