From 802366bdf00adf3849499f43ba07ee726da0668a Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 19 May 2016 07:41:09 +0200
Subject: coqc: support -o option to specify output file name

The -o option lets one put .vo or .vio files in a directory of choice,
i.e. decouple the location of the sources and the compiled files.
This ease the integration of Coq in already existing IDEs that handle
the build process automatically (eg Eclipse) and also enables one to
compile/run at the same time 2 versions of Coq on the same sources.

Example: b.v depending on a.v

  coq8.6/bin/coqc -R out8.6 Test src/a.v -o out8.6/a.vo
  coq8.6/bin/coqc -R out8.6 Test src/b.v -o out8.6/b.vo

  coq8.7/bin/coqc -R out8.7 Test src/a.v -o out8.7/a.vo
  coq8.7/bin/coqc -R out8.7 Test src/b.v -o out8.7/b.vo
---
 stm/stm.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'stm')

diff --git a/stm/stm.ml b/stm/stm.ml
index 8f11875b62..ebafed8d37 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2108,11 +2108,11 @@ let handle_failure (e, info) vcs tty =
       VCS.print ();
       iraise (e, info)
 
-let snapshot_vio ldir long_f_dot_v =
+let snapshot_vio ldir long_f_dot_vo =
   finish ();
   if List.length (VCS.branches ()) > 1 then
     Errors.errorlabstrm "stm" (str"Cannot dump a vio with open proofs");
-  Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_v
+  Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo
     (Global.opaque_tables ())
 
 let reset_task_queue = Slaves.reset_task_queue
-- 
cgit v1.2.3