# HG changeset patch # User wenzelm # Date 1246809207 -7200 # Node ID 9560a458efed6f88fa25672c31159ee95e356b9c # Parent f6f124c9b63b98ba3a41cecb3504eea3ac7e94d5 updated to jedit 4.3pre17 -- no longer provide separate ml.xml; diff -r f6f124c9b63b -r 9560a458efed src/Tools/jEdit/dist-template/modes/catalog-template --- a/src/Tools/jEdit/dist-template/modes/catalog-template Sun Jul 05 17:26:14 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,10 +0,0 @@ - - - - - - - - - - diff -r f6f124c9b63b -r 9560a458efed src/Tools/jEdit/dist-template/modes/ml.xml --- a/src/Tools/jEdit/dist-template/modes/ml.xml Sun Jul 05 17:26:14 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,211 +0,0 @@ - - - - - - - - - - - - - - - - - - - (* - *) - - - - - #" - " - - - - - " - " - - - - - - / - * - - - + - - - ^ - @ - = - < - > - ( - ) - [ - ] - { - } - , - : - ; - | - # - - - fun - val - exception - - type - abstype - eqtype - datatype - - functor - structure - signature - - - - - - - div - mod - - - o - - - before - - - abstype - datatype - eqtype - type - - - exception - fun - val - fn - - - and - end - in - infix - infixr - let - local - as - of - op - - - functor - include - open - sharing - sig - signature - struct - structure - where - with - - - andalso - orelse - else - if - case - handle - raise - then - - - do - nonfix - rec - withtype - while - - - array - bool - char - exn - frag - int - list - option - order - real - ref - string - substring - unit - vector - word - word8 - - - Bind - Chr - Domain - Div - Fail - Graphic - Interrupt - Io - Match - Option - Ord - Overflow - Size - Subscript - SysErr - - - false - true - QUOTE - ANTIQUOTE - nil - NONE - SOME - LESS - EQUAL - GREATER - - - - \ No newline at end of file diff -r f6f124c9b63b -r 9560a458efed src/Tools/jEdit/makedist --- a/src/Tools/jEdit/makedist Sun Jul 05 17:26:14 2009 +0200 +++ b/src/Tools/jEdit/makedist Sun Jul 05 17:53:27 2009 +0200 @@ -11,7 +11,7 @@ ## diagnostics -JEDIT_HOME="/home/isajedit/jedit-orig/4.3pre16" +JEDIT_HOME="/home/isajedit/jedit-orig/4.3pre17" function usage() { @@ -89,6 +89,7 @@ print qq,\n\n,; } print; }' "$JEDIT/modes/catalog" + # build archive echo "${JEDIT}.tar.gz"