Skip to content

Commit 07f7d3a

Browse files
committed
dune autoconfigure: use relocatable mode
1 parent a43a641 commit 07f7d3a

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

config/dune

+1-1
Original file line numberDiff line numberDiff line change
@@ -36,4 +36,4 @@
3636
%{project_root}/dev/header.c
3737
; Needed to generate include lists for coq_makefile
3838
plugin_list)
39-
(action (chdir %{project_root} (run %{project_root}/tools/configure/configure.exe -quiet -prefix %{workspace_root}/../install/default))))
39+
(action (chdir %{project_root} (run %{project_root}/tools/configure/configure.exe -quiet -relocatable))))

0 commit comments

Comments
 (0)