| 123456789101112131415161718 |
- Index: install.ml
- --- install.ml.orig 2008-05-26 12:49:40 +0200
- +++ install.ml 2008-05-30 11:43:14 +0200
- @@ -161,10 +161,10 @@
- in
- let startdir = Sys.getcwd() in
- try
- - download();
- + (* download(); *)
- compile();
- Sys.chdir startdir;
- with
- Failure msg ->
- Sys.chdir startdir;
- - prerr_endline msg; exit 1
- \ No newline at end of file
- + prerr_endline msg; exit 1
|
