# 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"