| changeset 44661 | 383c9d758a56 |
| parent 44549 | 5e5e6ad3922c |
| child 44676 | 7de87f1ae965 |
--- a/src/Pure/General/markup.scala Fri Sep 02 21:06:05 2011 +0200 +++ b/src/Pure/General/markup.scala Fri Sep 02 21:48:27 2011 +0200 @@ -273,6 +273,8 @@ val FUNCTION = "function" val Function = new Properties.String(FUNCTION) + val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs")) + val INVOKE_SCALA = "invoke_scala" object Invoke_Scala {