aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2015-12-14 14:30:44 +0100
committerGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2015-12-14 14:30:44 +0100
commite0e2ceaa1bc1750fc05b4589351e10a1081453dd (patch)
tree23ab09d7d5ff7969068e23c96c58c805f41d8884 /generic
parentb957a9049f64bfe3352b148046df94aa1baf5613 (diff)
Small refactoring of coqxxx args detection.
Need some more refactoring actually: Some code from coq-compile-common became necessary to coq/pg globally. We shoudl refelct this by moving these parts somewhere else.
Diffstat (limited to 'generic')
0 files changed, 0 insertions, 0 deletions