aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
Diffstat (limited to 'driver')
-rw-r--r--driver/Frontend.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/Frontend.ml b/driver/Frontend.ml
index 0d0ff26c..480932df 100644
--- a/driver/Frontend.ml
+++ b/driver/Frontend.ml
@@ -119,6 +119,7 @@ let init () =
else Machine.rv32
| "kvx" -> if Configuration.os = "cos" then Machine.kvxcos
else if Configuration.os = "mbr" then Machine.kvxmbr
+ else if Configuration.os = "elf" then Machine.kvxelf
else (Printf.eprintf "Configuration OS = %s\n" Configuration.os;
failwith "Wrong OS configuration for KVX")
| "aarch64" -> if Configuration.abi = "apple"