diff --git a/configure b/configure index 0c44fe0..905185b 100755 --- a/configure +++ b/configure @@ -80,7 +80,7 @@ while : ; do -mpi|--mpi) mpi='-tag "package(mpi)"';; -profile|--profile) - ocamloptflags=$ocamloptflags_profile + ocamloptflags=$ocamloptflags_profile;; -h|-help|--help) help;; *)