Updated configure

2025-01-03 10:05:40 +01:00 · 2019-04-04 00:38:57 +02:00 · 2019-04-04 00:38:57 +02:00 · 72422d84b5
commit 72422d84b5
parent 1933e560d2
1 changed files with 1 additions and 1 deletions
--- a/2
+++ b/2
@ -80,7 +80,7 @@ while : ; do
        -mpi|--mpi)
            mpi='-tag "package(mpi)"';;
        -profile|--profile)
-            ocamloptflags=$ocamloptflags_profile
+            ocamloptflags=$ocamloptflags_profile;;
        -h|-help|--help)
            help;;
        *)