| changeset 49004 | 3a324a3f4aea |
| parent 48972 | 196520d51afd |
| child 50647 | 58312dae25a5 |
| 49003:09a9761cf5ae | 49004:3a324a3f4aea |
|---|---|
44 |
44 |
45 |
45 |
46 Packaging |
46 Packaging |
47 ========= |
47 ========= |
48 |
48 |
49 - makedist -j jedit_build-XXXX -r DISTNAME |
49 - hg up -r DISTNAME && isabelle makedist -r DISTNAME; |
50 |
50 |
51 - makebin (multiplatform); |
51 - makebin (multiplatform); |
52 |
52 |
53 - makebundle (multiplatform); |
53 - makebundle (multiplatform); |
54 |
54 |