Skip to content

Some simplifications and improvements to the configure script#132

Merged
xavierleroy merged 3 commits intoocaml:masterfrom
xavierleroy:configure-revised
Jul 18, 2023
Merged

Some simplifications and improvements to the configure script#132
xavierleroy merged 3 commits intoocaml:masterfrom
xavierleroy:configure-revised

Commits

Commits on Jul 18, 2023