git.annexia.org
/
goaljobs.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
05f0550
)
example: Remove code which is now implicitly generated.
author
Richard W.M. Jones
<rjones@redhat.com>
Tue, 17 Sep 2013 11:31:17 +0000
(12:31 +0100)
committer
Richard W.M. Jones
<rjones@redhat.com>
Tue, 17 Sep 2013 11:38:01 +0000
(12:38 +0100)
examples/compile-c/compile.ml
patch
|
blob
|
history
diff --git
a/examples/compile-c/compile.ml
b/examples/compile-c/compile.ml
index
8e43948
..
151e8b7
100644
(file)
--- a/
examples/compile-c/compile.ml
+++ b/
examples/compile-c/compile.ml
@@
-17,14
+17,3
@@
and compiled c_file =
target (more_recent [o_file] [c_file]);
require (file_exists c_file);
sh "cd $builddir && cc -c %s -o %s" c_file o_file
-
-(* XXX IMPLICIT *)
-let () =
- try goal_all ()
- with
- | Goal_result (Goal_failed msg) ->
- prerr_endline ("error: " ^ msg);
- exit 1
- | exn ->
- prerr_endline (Printexc.to_string exn);
- exit 1