From 7abc2cdab5f3ff0da49056f93ecbd02d2c1704c5 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 31 Mar 2022 10:59:44 +0200
Subject: [PATCH] Add current directory as default loadpath.
---
src/main.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/main.ml b/src/main.ml
index 9a9b01a8..bc097c4e 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -127,7 +127,7 @@ let verify_cmd =
in
let loadpath =
let doc = "Additional loadpath." in
- Arg.(value & opt_all string [] & info [ "L" ] ~doc)
+ Arg.(value & opt_all string [ "." ] & info [ "L"; "loadpath" ] ~doc)
in
let memlimit =
let doc = "Memory limit (in megabytes)." in
--
GitLab