From 72422d84b5d6dfca88e1c6629a5479f9551a210f Mon Sep 17 00:00:00 2001 From: Anthony Scemama Date: Thu, 4 Apr 2019 00:38:57 +0200 Subject: [PATCH] Updated configure --- configure | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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;; *)