aboutsummaryrefslogtreecommitdiffstats
path: root/exportclight
diff options
context:
space:
mode:
authorDavid Monniaux <David.Monniaux@univ-grenoble-alpes.fr>2021-09-27 20:47:49 +0200
committerDavid Monniaux <David.Monniaux@univ-grenoble-alpes.fr>2021-09-27 20:47:49 +0200
commitd757b0b46458ca4f67080c84755b086f6e700b70 (patch)
tree5f0bc752e9eeda4f0a2847802a246141f3cfa8ac /exportclight
parent79c1aed726d9532125305af52ecbb010847a8a2c (diff)
downloadcompcert-kvx-d757b0b46458ca4f67080c84755b086f6e700b70.tar.gz
compcert-kvx-d757b0b46458ca4f67080c84755b086f6e700b70.zip
better fail
Diffstat (limited to 'exportclight')
-rw-r--r--exportclight/ExportClight.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index 9937e5e7..e6d08d4f 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -288,7 +288,7 @@ let external_function p = function
signatur sg
(print_list coqstring) clob
| EF_profiling(id, kind) ->
- fprintf p "EF_profiling" (* should not happen *)
+ failwith "EF_profiling in ExportClight" (* should not happen *)
(* Expressions *)