diff options
| -rwxr-xr-x | debian/rules | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/debian/rules b/debian/rules index bf3d4cbb..04a75b29 100755 --- a/debian/rules +++ b/debian/rules @@ -37,7 +37,7 @@ CONFIGUREOPTS := --arch Linux --prefix /usr --mandir /usr/share/man \ --browser "/usr/bin/x-www-browser %s &" \ --with-doc no --coqrunbyteflags "-dllib -lcoqrun" -OCAMLINITSED := -e 's/@OCamlDllDir@/$(OCAML_DLL_DIR)/g' -e -e '/^\#/d' +OCAMLINITSED := -e 's%@OCamlDllDir@%$(OCAML_DLL_DIR)%g' -e '/^\#/d' ifneq ($(OCAML_OPT_ARCH),) # CONFIGUREOPTS += -opt |