aboutsummaryrefslogtreecommitdiffhomepage
path: root/config
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-01-11 08:24:23 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-01-11 08:24:23 +0000
commit2c72ac19c3321100b542d68773e2725cbf33dc3f (patch)
tree726f83454a9bfb46d75adec6c9e89d81a2ef8e69 /config
parentabdfeedd0047ea94913b328d63d23989afd886ad (diff)
Pour déterminer sous Windows si ocaml est en version cygwin ou win32
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2391 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'config')
-rw-r--r--config/giveostype.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/config/giveostype.ml b/config/giveostype.ml
new file mode 100644
index 000000000..e657bc79f
--- /dev/null
+++ b/config/giveostype.ml
@@ -0,0 +1 @@
+print_string Sys.os_type;;